From 76d91f7d2bc7b56ab394a6be2bf6f1ebeef8e561 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 4 Mar 2020 14:27:32 -0800
Subject: [PATCH] fix #3142

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bv_rewriter.cpp | 3 ++-
 src/sat/sat_solver.cpp           | 7 +++++++
 src/sat/sat_unit_walk.h          | 1 +
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 896f4b9aa..62fe2e9bd 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2602,13 +2602,14 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
     }
 
     br_status st;
-    if (m_bit2bool) {
+    if (m_bit2bool && false) {
         st = mk_bit2bool(lhs, rhs, result);
         if (st != BR_FAILED)
             return st;
     }
 
     if (m_trailing) {
+        
         st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result);
         m_rm_trailing.reset_cache(1 << 12);
         if (st != BR_FAILED) {
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 8f3704d59..b6ad3eb98 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1317,6 +1317,13 @@ namespace sat {
     lbool solver::do_unit_walk() {
         unit_walk srch(*this);
         lbool r = srch();
+        if (r == l_true) {
+            m_model.reset();
+            for (bool_var v = 0; v < num_vars(); ++v) {
+                m_model.push_back(m_assignment[literal(v,false).index()]);
+            }
+            m_model_is_current = true;
+        }
         return r;
     }
 
diff --git a/src/sat/sat_unit_walk.h b/src/sat/sat_unit_walk.h
index 14588a63c..2b2e35b6d 100644
--- a/src/sat/sat_unit_walk.h
+++ b/src/sat/sat_unit_walk.h
@@ -71,6 +71,7 @@ namespace sat {
         bool              m_inconsistent;
         literal_vector    m_decisions;
         unsigned          m_conflict_offset;
+        svector<lbool>    m_model;
 
         bool should_restart();
         void do_pop();