Merge branch 'master' into dspil_benchmarking

src/main/scala/Config.scala

@@ -822,12 +822,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

@@ -414,7 +414,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/supporters/BuiltinDomainsContributor.scala

@@ -17,7 +17,6 @@ import viper.silicon.interfaces.PreambleContributor
 import viper.silicon.interfaces.decider.ProverLike
 import viper.silicon.state.DefaultSymbolConverter
 import viper.silicon.state.terms._
-import viper.silver.ast.LineCol
 
 abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, DomainFun, Term] {
   type BuiltinDomainType <: ast.GenericType
@@ -194,23 +193,14 @@ private object utils {
       }
 
     val fp = new viper.silver.parser.FastParser()
-    val lc = new LineCol(fp)
-    fp.parse(content, fromPath) match {
-      case fastparse.Parsed.Success(parsedProgram: viper.silver.parser.PProgram, _) =>
-        assert(parsedProgram.errors.isEmpty, s"Unexpected parsing errors: ${parsedProgram.errors}")
-
-        val resolver = viper.silver.parser.Resolver(parsedProgram)
-        val resolved = resolver.run.get
-        val translator = viper.silver.parser.Translator(resolved)
-        val program = translator.translate.get
-
-        program
-
-      case fastparse.Parsed.Failure(msg, index, _) =>
-        val (line, col) = lc.getPos(index)
-        sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, line, col)}")
-        //? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt)
-        //? sys.error(s"Failure: $msg, at ${viper.silver.ast.FilePosition(fromPath, pos(0), pos(1))}")
-    }
+    val parsedProgram = fp.parse(content, fromPath)
+    assert(parsedProgram.errors.isEmpty, s"Unexpected parsing errors: ${parsedProgram.errors}")
+
+    val resolver = viper.silver.parser.Resolver(parsedProgram)
+    val resolved = resolver.run.get
+    val translator = viper.silver.parser.Translator(resolved)
+    val program = translator.translate.get
+
+    program
   }
 }