disable multi-threading for validation code, masks #4196

NikolajBjorner · NikolajBjorner · commit 91a190a7854a · 2020-05-03T10:37:29.000-07:00
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) {

Original file line number	Diff line number	Diff line change
`@@ -385,8 +385,7 @@ namespace smt {`
`385`	`385`	`TRACE("context", tout << "inconsistent\n";);`
`386`	`386`	`SASSERT(inconsistent());`
`387`	`387`	`m_conflict = null_b_justification;`
`388`		`- m_not_l = null_literal;`
`389`		`- SASSERT(m_search_lvl == get_search_level());`
	`388`	`+ m_not_l = null_literal;`
`390`	`389`	`}`
`391`	`390`	`}`
`392`	`391`	`}`
`@@ -619,6 +618,7 @@ namespace smt {`
`619`	`618`	`//`
`620`	`619`	`void context::validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars,`
`621`	`620`	`expr_ref_vector const& conseq, expr_ref_vector const& unfixed) {`
	`621`	`+ m_fparams.m_threads = 1;`
`622`	`622`	`expr_ref tmp(m);`
`623`	`623`	`SASSERT(!inconsistent());`
`624`	`624`	`for (expr* c : conseq) {`