diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
index 78a3e498..5db6534c 100644
--- 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
index 152bf1d6..035de897 100644
--- 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"))
     }
   }