Undo merge strangeness

src/main/scala/Config.scala

@@ -816,12 +816,6 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     case _ => Right(())
   }
 
-  validateOpt(assertionMode, parallelizeBranches) {
-    case (Some(AssertionMode.SoftConstraints), Some(true)) =>
-      Left(s"Assertion mode SoftConstraints is not supported in combination with ${parallelizeBranches.name}")
-    case _ => Right()
-  }
-
   validateFileOpt(logConfig)
   validateFileOpt(setAxiomatizationFile)
   validateFileOpt(multisetAxiomatizationFile)

src/main/scala/decider/Decider.scala

@@ -382,7 +382,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def statistics(): Map[String, String] = prover.statistics()
 
-    override def generateModel(): Unit = proverAssert(False, None)
+    override def generateModel(): Unit = proverAssert(False, Verifier.config.assertTimeout.toOption)
 
     override def getModel(): Model = prover.getModel()
 

src/main/scala/decider/Z3ProverAPI.scala

@@ -9,19 +9,17 @@ package viper.silicon.decider
 import com.typesafe.scalalogging.LazyLogging
 import viper.silicon.common.config.Version
 import viper.silicon.interfaces.decider.{Prover, Result, Sat, Unknown, Unsat}
-import viper.silicon.state.{IdentifierFactory, State}
-import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, Ite, MacroDecl, Quantification, Sort, SortDecl, SortWrapperDecl, Term, Trigger, TriggerGenerator, sorts}
+import viper.silicon.state.IdentifierFactory
+import viper.silicon.state.terms.{App, Decl, Fun, FunctionDecl, Implies, MacroDecl, Not, Quantification, Sort, SortDecl, SortWrapperDecl, Term, TriggerGenerator, sorts}
 import viper.silicon.{Config, Map}
 import viper.silicon.verifier.Verifier
 import viper.silver.reporter.{InternalWarningMessage, Reporter}
 import viper.silver.verifier.{MapEntry, ModelEntry, ModelParser, ValueEntry, DefaultDependency => SilDefaultDependency, Model => ViperModel}
 
-import java.io.PrintWriter
 import java.nio.file.Path
 import scala.collection.mutable
 import com.microsoft.z3._
 import com.microsoft.z3.enumerations.Z3_param_kind
-import viper.silicon.decider.Z3ProverAPI.oldVersionOnlyParams
 import viper.silicon.reporting.ExternalToolError
 
 import scala.jdk.CollectionConverters.MapHasAsJava
@@ -64,7 +62,6 @@ object Z3ProverAPI {
     "smt.qi.eager_threshold" -> 100.0,
   )
   val allParams = boolParams ++ intParams ++ stringParams ++ doubleParams
-  val oldVersionOnlyParams = Set("smt.arith.solver")
 }
 
 
@@ -122,26 +119,21 @@ class Z3ProverAPI(uniqueId: String,
         s
     }
 
-    val useOldVersionParams = version() <= Version("4.8.7.0")
     Z3ProverAPI.boolParams.foreach{
       case (k, v) =>
-        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
-          params.add(removeSmtPrefix(k), v)
+        params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.intParams.foreach{
       case (k, v) =>
-        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
-          params.add(removeSmtPrefix(k), v)
+        params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.doubleParams.foreach{
       case (k, v) =>
-        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
-          params.add(removeSmtPrefix(k), v)
+        params.add(removeSmtPrefix(k), v)
     }
     Z3ProverAPI.stringParams.foreach{
       case (k, v) =>
-        if (useOldVersionParams || !oldVersionOnlyParams.contains(k))
-          params.add(removeSmtPrefix(k), v)
+        params.add(removeSmtPrefix(k), v)
     }
     val userProvidedArgs = Verifier.config.proverConfigArgs
     prover = ctx.mkSolver()
@@ -256,19 +248,24 @@ class Z3ProverAPI(uniqueId: String,
         // When used via API, Z3 completely discards assumptions that contain invalid triggers (whereas it just ignores
         // the invalid trigger when used via stdio). Thus, to make sure our assumption is not discarded, we manually
         // walk through all quantifiers and remove invalid terms inside the trigger.
-        triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger)
-        val cleanTerm = term.transform{
-          case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty =>
-            val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect{
-              case t => triggerGenerator.isForbiddenInTrigger(t)
-            }.nonEmpty))
-            q.copy(triggers = goodTriggers)
-        }()
+        val cleanTerm = cleanTriggers(term)
         prover.add(termConverter.convert(cleanTerm).asInstanceOf[BoolExpr])
         reporter.report(InternalWarningMessage("Z3 error: " + e.getMessage))
     }
   }
 
+  def cleanTriggers(term: Term): Term = {
+    triggerGenerator.setCustomIsForbiddenInTrigger(triggerGenerator.advancedIsForbiddenInTrigger)
+    val cleanTerm = term.transform {
+      case q@Quantification(_, _, _, triggers, _, _, _) if triggers.nonEmpty =>
+        val goodTriggers = triggers.filterNot(trig => trig.p.exists(ptrn => ptrn.shallowCollect {
+          case t => triggerGenerator.isForbiddenInTrigger(t)
+        }.nonEmpty))
+        q.copy(triggers = goodTriggers)
+    }()
+    cleanTerm
+  }
+
   def assert(goal: Term, timeout: Option[Int]): Boolean = {
     endPreamblePhase()
 
@@ -279,7 +276,14 @@ class Z3ProverAPI(uniqueId: String,
       }
       result
     } catch {
-      case e: Z3Exception => throw ExternalToolError("Prover", "Z3 error: " + e.getMessage)
+      case e: Z3Exception => {
+        val cleanGoal = cleanTriggers(goal)
+        if (cleanGoal == goal) {
+          throw ExternalToolError("Prover", "Z3 error: " + e.getMessage)
+        } else {
+          assert(cleanGoal, timeout)
+        }
+      }
     }
   }
 
@@ -342,7 +346,7 @@ class Z3ProverAPI(uniqueId: String,
 
     val guard = fresh("grd", Nil, sorts.Bool)
     val guardApp = App(guard, Nil)
-    val goalImplication = Implies(guardApp, goal)
+    val goalImplication = Implies(guardApp, Not(goal))
 
     prover.add(termConverter.convertTerm(goalImplication).asInstanceOf[BoolExpr])
 

src/main/scala/rules/Evaluator.scala

@@ -291,9 +291,9 @@ object evaluator extends EvaluationRules {
 
       case ast.Let(x, e0, e1) =>
         eval(s, e0, pve, v)((s1, t0, v1) => {
-          val t = v1.decider.fresh(v1.symbolConverter.toSort(x.typ))
+          val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables)
           v1.decider.assume(t === t0)
-          val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t)
+          val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function])
           eval(s1.copy(g = s1.g + (x.localVar, t0), functionRecorder = newFuncRec), e1, pve, v1)(Q)
         })
 

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -1362,9 +1362,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       // ME: When using Z3 via API, it is beneficial to not use macros, since macro-terms will *always* be different
       // (leading to new terms that have to be translated), whereas without macros, we can usually use a term
       // that already exists.
+      // ME: Update: Actually, it seems better to use macros even with the API since Silicon terms can grow so large
+      // that e.g. the instantiate call in createPermissionConstraintAndDepletedCheck takes forever, before even
+      // converting to a Z3 term.
       // During function verification, we should not define macros, since they could contain resullt, which is not
       // defined elsewhere.
-      val declareMacro = s.functionRecorder == NoopFunctionRecorder && !Verifier.config.useFlyweight
+      val declareMacro = s.functionRecorder == NoopFunctionRecorder // && !Verifier.config.useFlyweight
 
       val permsProvided = ch.perm
       val permsTaken = if (declareMacro) {

src/main/scala/supporters/Domains.scala

@@ -12,9 +12,9 @@ import viper.silicon.common.collections.immutable.MultiMap._
 import viper.silicon.toMap
 import viper.silicon.interfaces.PreambleContributor
 import viper.silicon.interfaces.decider.ProverLike
-import viper.silicon.state.{SymbolConverter, terms}
+import viper.silicon.state.{FunctionPreconditionTransformer, SymbolConverter, terms}
 import viper.silicon.state.terms.{Distinct, DomainFun, Sort, Term}
-import viper.silver.ast.{NamedDomainAxiom}
+import viper.silver.ast.NamedDomainAxiom
 
 trait DomainsContributor[SO, SY, AX, UA] extends PreambleContributor[SO, SY, AX] {
   def uniquenessAssumptionsAfterAnalysis: Iterable[UA]
@@ -100,7 +100,8 @@ class DefaultDomainsContributor(symbolConverter: SymbolConverter,
 
       domain.axioms foreach (axiom => {
         val tAx = domainTranslator.translateAxiom(axiom, symbolConverter.toSort)
-        collectedAxioms += tAx
+        val tAxPres = FunctionPreconditionTransformer.transform(tAx, program)
+        collectedAxioms += terms.And(tAxPres, tAx)
       })
     })
   }

src/main/scala/supporters/ExpressionTranslator.scala

@@ -162,14 +162,23 @@ trait ExpressionTranslator {
         val df = Fun(id, inSorts, outSort)
         App(df, tArgs)
 
-      case bfa@ast.BackendFuncApp(func, args) =>
+      case bfa@ast.BackendFuncApp(_, args) =>
         val tArgs = args map f
         val inSorts = tArgs map (_.sort)
         val outSort = toSort(bfa.typ)
         val id = Identifier(bfa.interpretation)
         val sf = SMTFun(id, inSorts, outSort)
         App(sf, tArgs)
 
+      case fa@ast.FuncApp(name, args) =>
+        // We are assuming here that only functions with empty preconditions are used.
+        val tArgs = Unit +: (args map f)
+        val inSorts = tArgs map (_.sort)
+        val outSort = toSort(fa.typ)
+        val id = Identifier(name)
+        val df = HeapDepFun(id, inSorts, outSort)
+        App(df, tArgs)
+
       /* Permissions */
 
       case _: ast.FullPerm => FullPerm