disable multi-threading for validation code, masks Z3Prover#4196

hgvk94 · May 7, 2020 · 2c0a221 · 2c0a221
1 parent 057fed0
commit 2c0a221
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
@@ -385,8 +385,7 @@ namespace smt {
                         TRACE("context", tout << "inconsistent\n";);
                         SASSERT(inconsistent());
                         m_conflict = null_b_justification;
-                        m_not_l = null_literal;
-                        SASSERT(m_search_lvl == get_search_level());                    
+                        m_not_l = null_literal;                   
                     }
                 }
             }
@@ -619,6 +618,7 @@ namespace smt {
     // 
     void context::validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
                                         expr_ref_vector const& conseq, expr_ref_vector const& unfixed) {
+        m_fparams.m_threads = 1;
         expr_ref tmp(m);
         SASSERT(!inconsistent());
         for (expr* c : conseq) {