Supporting MWSF in Z3 API (#859)

Supporting MWSF in Z3 API, fixing prover options reset in test suite
viperproject · Jul 1, 2024 · 46a35ff · 46a35ff
1 parent 1b11869
commit 46a35ff
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
@@ -204,6 +204,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       _declaredFreshMacros = Vector.empty
       _freshMacroStack = Stack.empty
       _freshFunctionStack = Stack.empty
+      _proverOptions = Map.empty
     }
 
     def stop(): Unit = {

diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala
@@ -128,6 +128,7 @@ class TermToZ3APIConverter
 
       case sorts.FieldPermFunction() => ctx.mkUninterpretedSort("$FPM") // text("$FPM")
       case sorts.PredicatePermFunction() => ctx.mkUninterpretedSort("$PPM") // text("$PPM")
+      case sorts.MagicWandSnapFunction => ctx.mkUninterpretedSort("$MWSF")
     }
     sortCache.update(s, res)
     res
@@ -159,6 +160,7 @@ class TermToZ3APIConverter
 
       case sorts.FieldPermFunction() => Some(ctx.mkSymbol("$FPM")) // text("$FPM")
       case sorts.PredicatePermFunction() => Some(ctx.mkSymbol("$PPM")) // text("$PPM")
+      case sorts.MagicWandSnapFunction => Some(ctx.mkSymbol("$MWSF"))
     }
   }