Merge pull request #737 from viperproject/meilers_let_in_quant

Fixing unsound assumption about helper variable inside quantifiers
viperproject · Jul 4, 2023 · 2d7d6cf · 2d7d6cf
2 parents 442ed9c + 694756f
commit 2d7d6cf
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/main/scala/rules/Evaluator.scala b/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)
         })