smt: set Z3's smtlib2_compliant=true

This disables some type coersion checks, so we get a bit of a speedup
AliveToolkit · Dec 22, 2023 · 13266e9 · 13266e9
1 parent 06de006
commit 13266e9
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/smt/ctx.cpp b/smt/ctx.cpp
@@ -31,6 +31,7 @@ void context::init() {
   Z3_global_param_set("model.partial", "true");
   Z3_global_param_set("smt.ematching", "false");
   Z3_global_param_set("smt.mbqi.max_iterations", "1000000");
+  Z3_global_param_set("smtlib2_compliant", "true");
   Z3_global_param_set("smt.random_seed", get_random_seed());
   Z3_global_param_set("timeout", get_query_timeout());
   Z3_global_param_set("memory_high_watermark", "2147483648"); // 2 GBs