Skip to content

Commit 071af4a

Browse files
committed
SMTFuncApps are no longer PossibleTriggers
1 parent 16c0299 commit 071af4a

1 file changed

Lines changed: 1 addition & 3 deletions

File tree

src/main/scala/viper/silver/ast/Expression.scala

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -391,10 +391,8 @@ object DomainFuncApp {
391391

392392
case class SMTFuncApp(smtfunc: SMTFunc, args: Seq[Exp])
393393
(val pos: Position, val info: Info, override val typ : Type, val errT: ErrorTrafo)
394-
extends AbstractDomainFuncApp with PossibleTrigger {
394+
extends AbstractDomainFuncApp {
395395
override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
396-
def getArgs = args
397-
def withArgs(newArgs: Seq[Exp]) = SMTFuncApp(smtfunc, newArgs)(pos,info,typ, errT)
398396
override def func = (p: Program) => smtfunc
399397
def funcname = smtfunc.name
400398
}

0 commit comments

Comments
 (0)