From 91a190a7854afee414bc58f84f4ebbc2ea83de59 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 3 May 2020 10:37:29 -0700
Subject: [PATCH] disable multi-threading for validation code, masks #4196

---
 src/smt/smt_consequences.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index cb11ec70f..989d42d7b 100644
--- 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) {