Various updates in preparation for Z3 version update

src/main/scala/viper/carbon/boogie/boogie.scala

@@ -359,6 +359,15 @@ case class If(cond: Exp, thn: Stmt, els: Stmt) extends Stmt
 case class Seqn(stmts: Seq[Stmt]) extends Stmt
 /** A non-deterministic if statement. */
 case class NondetIf(thn: Stmt, els: Stmt = Statements.EmptyStmt) extends Stmt
+
+/**
+  * Execute a statement (usually an Assert) locally in a new branch that is subsequently killed.
+  */
+object Locally {
+  def apply(stmt: Stmt) = {
+      NondetIf(Seqn(Seq(stmt, Assume(FalseLit()))))
+  }
+}
 /**
  * Something like a 'declaration' of a local variable that allows to specify a where
  * clause.  However, local variables do not need to be declared if no where clause

src/main/scala/viper/carbon/modules/impls/DefaultHeapModule.scala

@@ -447,35 +447,38 @@ class DefaultHeapModule(val verifier: Verifier)
     val pmT = predicateMaskFieldTypeOf(p)
     val varDecls = p.formalArgs map mainModule.translateLocalVarDecl
     val vars = varDecls map (_.l)
+    val predArgGetters = varDecls.map (v => Func(Identifier(f"predicate_${p.name}_arg_${v.name.name}"), Seq(LocalVarDecl(Identifier("pred"), t)), v.typ))
+    val predArgGetters2 = varDecls.map (v => Func(Identifier(f"predicate_${p.name}_arg_${v.name.name}_sm"), Seq(LocalVarDecl(Identifier("pred"), pmT)), v.typ))
     val predId:BigInt = getPredicateOrWandId(p.name)
     val f0 = FuncApp(predicate, vars, t)
     val f1 = predicateMaskField(f0)
     val f2 = FuncApp(pmField, vars, pmT)
     TypeDecl(predicateMetaTypeOf(p)) ++
       Func(predicate, varDecls, t) ++
       Func(pmField, varDecls, pmT) ++
+      predArgGetters ++
+      predArgGetters2 ++
       Axiom(MaybeForall(varDecls, Trigger(f1), f1 === f2)) ++
       Axiom(MaybeForall(varDecls, Trigger(f0), isPredicateField(f0))) ++
       Axiom(MaybeForall(varDecls, Trigger(f0), getPredicateOrWandId(f0) === IntLit(predId))) ++
       Func(predicateTriggerIdentifier(p), Seq(LocalVarDecl(heapName, heapTyp), LocalVarDecl(Identifier("pred"), predicateVersionFieldType())), Bool) ++
       Func(predicateTriggerAnyStateIdentifier(p), Seq(LocalVarDecl(Identifier("pred"), predicateVersionFieldType())), Bool) ++
       {
         // axiom that two predicate identifiers can only be the same, if all arguments
-        // are the same (e.g., we immediatly know that valid(1) != valid(2))
+        // are the same (e.g., we immediately know that valid(1) != valid(2))
         if (vars.size == 0) Nil
         else {
-          val varDecls2 = varDecls map (
-            v => LocalVarDecl(Identifier(v.name.name + "2")(v.name.namespace), v.typ))
-          val vars2 = varDecls2 map (_.l)
-          var varsEqual = All((vars zip vars2) map {
-            case (v1, v2) => v1 === v2
-          })
-          val f0_2 = FuncApp(predicate, vars2, t)
-          val f2_2 = FuncApp(pmField, vars2, t)
-          Axiom(Forall(varDecls ++ varDecls2, Trigger(Seq(f0, f0_2)),
-            (f0 === f0_2) ==> varsEqual)) ++
-            Axiom(Forall(varDecls ++ varDecls2, Trigger(Seq(f2, f2_2)),
-              (f2 === f2_2) ==> varsEqual))
+          val argGetApply = predArgGetters map (f => FuncApp(f.name, Seq(f0), f.typ))
+          val argGetEqual = argGetApply.zip(vars).map {
+            case (get, v) => get === v
+          }
+          val argGetAxiom = Axiom(Forall(varDecls, Trigger(f0), All(argGetEqual)))
+          val argGetApply2 = predArgGetters2 map (f => FuncApp(f.name, Seq(f2), f.typ))
+          val argGetEqual2 = argGetApply2.zip(vars).map {
+            case (get, v) => get === v
+          }
+          val argGetAxiom2 = Axiom(Forall(varDecls, Trigger(f2), All(argGetEqual2)))
+          argGetAxiom ++ argGetAxiom2
         }
       }
   }

src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala

@@ -620,8 +620,8 @@ class QuantifiedPermModule(val verifier: Verifier)
             //if the permission is a wildcard, we check that we have some permission > 0 for all locations and assume that the permission substracted is smaller than the permission held.
             val wildcardAssms:Stmt =
               if(isWildcard) {
-                (Assert(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(), translatedCond ==> (currentPermission(translatedRecv, translatedLocation) > noPerm)), error.dueTo(reasons.InsufficientPermission(fieldAccess))))++
-                  (Assume(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(), translatedCond ==> (wildcard < currentPermission(translatedRecv, translatedLocation)))))
+                Locally(Assert(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(), translatedCond ==> (currentPermission(translatedRecv, translatedLocation) > noPerm)), error.dueTo(reasons.InsufficientPermission(fieldAccess))))++
+                  (Assume(Forall(vsFresh.map(v => translateLocalVarDecl(v)), Seq(Trigger(currentPermission(translatedRecv, translatedLocation))), translatedCond ==> (wildcard < currentPermission(translatedRecv, translatedLocation)))))
               } else {
                 Nil
               }
@@ -673,13 +673,18 @@ class QuantifiedPermModule(val verifier: Verifier)
               CommentBlock("assume permission updates for independent locations", independentLocations) ++
               (mask := qpMask)
 
+            val inverseAssumptions: Stmt = if (assertReadPermOnly) Nil else
+              CommentBlock("assumptions for inverse of receiver " + recv.toString, Assume(invAssm1)++ Assume(invAssm2))
+
+            val checks = CommentBlock("check that the permission amount is positive", Locally(permPositive)) ++
+              CommentBlock("check if receiver " + recv.toString + " is injective", Locally(injectiveAssertion)) ++
+              CommentBlock("check if sufficient permission is held", Locally(enoughPerm))
+
             val res1 = Havoc(qpMask) ++
               MaybeComment("wild card assumptions", stmts ++
               wildcardAssms) ++
-              CommentBlock("check that the permission amount is positive", permPositive) ++
-              CommentBlock("check if receiver " + recv.toString + " is injective",injectiveAssertion) ++
-              CommentBlock("check if sufficient permission is held", enoughPerm) ++
-              CommentBlock("assumptions for inverse of receiver " + recv.toString, Assume(invAssm1)++ Assume(invAssm2)) ++
+              checks ++
+              inverseAssumptions ++
               maskUpdateStmt
 
             vsFresh.foreach(v => env.undefine(v.localVar))
@@ -793,8 +798,8 @@ class QuantifiedPermModule(val verifier: Verifier)
             //if we exhale a wildcard permission, assert that we hold some permission to all affected locations and restrict the wildcard value
             val wildcardAssms:Stmt =
               if(isWildcard) {
-                Assert(Forall(translatedLocals, Seq(), translatedCond ==> (currentPermission(translateNull, translatedResource) > noPerm)), error.dueTo(reason)) ++
-                  Assume(Forall(translatedLocals, Seq(), translatedCond ==> (wildcard < currentPermission(translateNull, translatedResource))))
+                Locally(Assert(Forall(translatedLocals, Seq(), translatedCond ==> (currentPermission(translateNull, translatedResource) > noPerm)), error.dueTo(reason))) ++
+                  Assume(Forall(translatedLocals, Seq(Trigger(currentPermission(translateNull, translatedResource))), translatedCond ==> (wildcard < currentPermission(translateNull, translatedResource))))
               } else {
                 Nil
               }
@@ -870,13 +875,18 @@ class QuantifiedPermModule(val verifier: Verifier)
               CommentBlock("assume permission updates for independent locations ", independentLocations) ++
               (mask := qpMask)
 
+            val inverseAssumptions: Stmt = if (assertReadPermOnly) Nil else
+              CommentBlock("assumptions for inverse of receiver " + accPred.toString, Assume(invAssm1)++ Assume(invAssm2))
+
+            val checks = CommentBlock("check that the permission amount is positive", Locally(permPositive)) ++
+              CommentBlock("check if receiver " + accPred.toString + " is injective", Locally(injectiveAssertion)) ++
+              CommentBlock("check if sufficient permission is held", Locally(enoughPerm))
+
             val res1 = Havoc(qpMask) ++
               MaybeComment("wildcard assumptions", stmts ++
               wildcardAssms) ++
-              CommentBlock("check that the permission amount is positive", permPositive) ++
-              CommentBlock("check if receiver " + accPred.toString + " is injective",injectiveAssertion) ++
-              CommentBlock("check if sufficient permission is held", enoughPerm) ++
-              CommentBlock("assumptions for inverse of receiver " + accPred.toString, Assume(invAssm1)++ Assume(invAssm2)) ++
+              checks ++
+              inverseAssumptions ++
               maskUpdateStmts
 
             vsFresh.foreach(vFresh => env.undefine(vFresh.localVar))
@@ -1248,15 +1258,15 @@ class QuantifiedPermModule(val verifier: Verifier)
 
            val reas = reasons.QPAssertionNotInjective(fieldAccess)
            var err = error.dueTo(reas)
-           val injectiveAssertion = Assert(is_injective, err)
+           val injectiveAssertion = Locally(Assert(is_injective, err))
 
            val res1 = Havoc(qpMask) ++
              stmts ++
              (if (!verifier.assumeInjectivityOnInhale) injectiveAssertion
              else Nil) ++
              CommentBlock("Define Inverse Function", Assume(invAssm1) ++
                Assume(invAssm2)) ++
-             (if (!isWildcard) MaybeComment("Check that permission expression is non-negative for all fields", permPositive) else Nil) ++
+             (if (!isWildcard) MaybeComment("Check that permission expression is non-negative for all fields", Locally(permPositive)) else Nil) ++
              CommentBlock("Assume set of fields is nonNull", nonNullAssumptions) ++
             // CommentBlock("Assume injectivity", injectiveAssumption) ++
              CommentBlock("Define permissions", Assume(Forall(obj, triggerForPermissionUpdateAxiom, condTrueLocations && condFalseLocations)) ++
@@ -1426,7 +1436,7 @@ class QuantifiedPermModule(val verifier: Verifier)
            }
            val injectTrigger = Seq(Trigger(Seq(triggerFunApp, triggerFunApp2)))
            val err = error.dueTo(reasons.QPAssertionNotInjective(accPred.loc))
-           val injectiveAssertion = Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), err)
+           val injectiveAssertion = Locally(Assert(Forall((translatedLocals ++ translatedLocals2), injectTrigger,injectiveCond ==> ineqExpr), err))
 
 
            val res1 = Havoc(qpMask) ++
@@ -1435,7 +1445,7 @@ class QuantifiedPermModule(val verifier: Verifier)
              else Nil) ++
              CommentBlock("Define Inverse Function", Assume(invAssm1) ++
                Assume(invAssm2)) ++
-             (if (!isWildcard) (MaybeComment("Check that permission expression is non-negative for all fields", permPositive)) else Nil) ++
+             (if (!isWildcard) (MaybeComment("Check that permission expression is non-negative for all fields", Locally(permPositive))) else Nil) ++
              CommentBlock("Define updated permissions", permissionsMap) ++
              CommentBlock("Define independent locations", (independentLocations ++
              independentResource)) ++

src/main/scala/viper/carbon/modules/impls/sequence_axioms/SequenceAxiomatization.scala

@@ -33,6 +33,7 @@ object SequenceAxiomatization {
                 | // diff 16 implemented: remove general cases of equality-learning between take/drop/append subsequences; only allow when take/drop are at top level (this affects linkedlists test case)
                 | // diff 17: removing a potential matching loop where more than one axiom applies to a Seq#Take(Seq#Append(s,t),n) term
                 | // diff 18: trying missing axioms for Take/Drop of at least full length
+                | // diff 19: removing a potential matching loop by making lhs of implication more explicit
                 |// START BASICS
                 |type Seq T;
                 |
@@ -82,8 +83,9 @@ object SequenceAxiomatization {
                 |axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) } // term below breaks loops
                 |  s0 != Seq#Empty() && s1 != Seq#Empty() && Seq#Length(s0) <= n && n < Seq#Length(Seq#Append(s0,s1)) ==> Seq#Add(Seq#Sub(n,Seq#Length(s0)),Seq#Length(s0)) == n && Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, Seq#Sub(n,Seq#Length(s0))));
                 |// AS: added "reverse triggering" versions of the axioms
+                |// ME: Added s_i != Seq#Append(s0,s1) on left hand side to make this condition explicit without requiring other axiom (diff 19)
                 |axiom (forall<T> s0: Seq T, s1: Seq T, m: int :: { Seq#Index(s1, m), Seq#Append(s0,s1)}  // m == n-|s0|, n == m + |s0|
-                |  s0 != Seq#Empty() && s1 != Seq#Empty() && 0 <= m && m < Seq#Length(s1) ==> Seq#Sub(Seq#Add(m,Seq#Length(s0)),Seq#Length(s0)) == m && Seq#Index(Seq#Append(s0,s1), Seq#Add(m,Seq#Length(s0))) == Seq#Index(s1, m));
+                |  s0 != Seq#Empty() && s1 != Seq#Empty() && s0 != Seq#Append(s0,s1) && s1 != Seq#Append(s0,s1) && 0 <= m && m < Seq#Length(s1) ==> Seq#Sub(Seq#Add(m,Seq#Length(s0)),Seq#Length(s0)) == m && Seq#Index(Seq#Append(s0,s1), Seq#Add(m,Seq#Length(s0))) == Seq#Index(s1, m));
                 |
                 |function Seq#Update<T>(Seq T, int, T): Seq T;
                 |axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) } {Seq#Length(s),Seq#Update(s,i,v)} // (diff 4: added trigger)
@@ -207,7 +209,7 @@ object SequenceAxiomatization {
                 |
                 |axiom (forall<T> s: Seq T, t: Seq T, n:int ::
                 |  { Seq#Drop(Seq#Append(s,t),n) }
-                | n > 0 && n > Seq#Length(s) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Drop(Seq#Append(s,t),n) == Seq#Drop(t,Seq#Sub(n,Seq#Length(s))));
+                | n > 0 && n > Seq#Length(s) && n < Seq#Length(Seq#Append(s,t)) ==> Seq#Add(Seq#Sub(n,Seq#Length(s)),Seq#Length(s)) == n && Seq#Drop(Seq#Append(s,t),n) == Seq#Drop(t,Seq#Sub(n,Seq#Length(s))));
                 |
                 |// diff 16: temporarily dropped general case of these
                 |//axiom (forall<T> s: Seq T, t: Seq T, m:int ::
@@ -335,11 +337,6 @@ object SequenceAxiomatization {
                 |*/
                 |// diff 9: skolemise equals (new)
                 |// AS: split axiom
-                |axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
-                |  Seq#Equal(s0,s1) ==>
-                |    Seq#Length(s0) == Seq#Length(s1) &&
-                |    (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
-                |        0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
                 |
                 |function Seq#SkolemDiff<T>(Seq T, Seq T) : int; // skolem function for Seq#Equals
                 |

src/main/scala/viper/carbon/verifier/BoogieInterface.scala

@@ -51,16 +51,10 @@ trait BoogieInterface {
     "/errorTrace:0",
     "/errorLimit:10000000",
     "/proverOpt:O:smt.AUTO_CONFIG=false",
-    "/proverOpt:O:smt.PHASE_SELECTION=0",
-    "/proverOpt:O:smt.RESTART_STRATEGY=0",
-    "/proverOpt:O:smt.RESTART_FACTOR=|1.5|",
-    "/proverOpt:O:smt.ARITH.RANDOM_INITIAL_VALUE=true",
     "/proverOpt:O:smt.CASE_SPLIT=3",
     "/proverOpt:O:smt.DELAY_UNITS=true",
-    "/proverOpt:O:NNF.SK_HACK=true",
     "/proverOpt:O:smt.MBQI=false",
     "/proverOpt:O:smt.QI.EAGER_THRESHOLD=100",
-    "/proverOpt:O:smt.BV.REFLECT=true",
     "/proverOpt:O:smt.qi.max_multi_patterns=1000",
     "/proverOpt:O:MODEL.PARTIAL=true",
     s"/proverOpt:PROVER_PATH=$z3Path")

src/test/scala/viper/carbon/AllTests.scala

@@ -40,5 +40,5 @@ class AllTests extends SilSuite {
   lazy val verifiers = List(verifier)
 
   val commandLineArguments: Seq[String] =
-    Seq()
+    Seq("--timeout=120")
 }