Test out a different z3 setting

utwente-fmt · Dec 5, 2024 · d0de091 · d0de091
1 parent 077f8b9
commit d0de091
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/viper/viper/api/backend/silicon/Silicon.scala b/src/viper/viper/api/backend/silicon/Silicon.scala
@@ -86,7 +86,8 @@ case class Silicon(
 
     val silicon = new viper.silicon.Silicon(reporter)
 
-    val z3Config = z3Settings.map { case (k, v) => s"$k=$v" }.mkString(" ")
+    val z3set = z3Settings ++ Seq(("smt.case_split","1"))
+    val z3Config = z3set.map { case (k, v) => s"$k=$v" }.mkString(" ")
 
     var siliconConfig = Seq(
       "--assertTimeout",