fix wrong condition for delayed bit-blasting

Z3Prover · Sep 3, 2022 · 60967ef · 60967ef
1 parent 0bdb2f1
commit 60967ef
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp
@@ -47,7 +47,7 @@ namespace bv {
             return true;
         unsigned num_vars = e->get_num_args();
         for (expr* arg : *e) 
-            if (!m.is_value(arg))
+            if (m.is_value(arg))
                 --num_vars;
         if (num_vars <= 1) 
             return true;