From 103ce78c29a4a2933637e0e6d4d5cb1fa5e6c08c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Nov 2017 08:53:06 -0800
Subject: [PATCH] save model from level 0, fix #1380

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/rewriter_def.h | 3 +++
 src/qe/qsat.cpp                 | 5 ++++-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 2abd6d467..31f7d4849 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -190,6 +190,9 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
         else if (m().is_false(cond)) {
             arg = t->get_arg(2);
         }
+        else {
+            std::cout << mk_ismt2_pp(cond, m()) << "\n";
+        }
         if (arg) {
             result_stack().shrink(fr.m_spos);
             result_stack().push_back(arg);
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 713ecfe77..2419d1c77 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -626,6 +626,9 @@ namespace qe {
                     SASSERT(validate_assumptions(*m_model.get(), asms));
                     SASSERT(validate_model(asms));
                     TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
+                    if (m_level == 0) {
+                        m_model_save = m_model;
+                    }
                     push();
                     if (m_level == 1 && m_mode == qsat_maximize) {
                         maximize_model();
@@ -1274,7 +1277,7 @@ namespace qe {
                 in->inc_depth();
                 result.push_back(in.get());
                 if (in->models_enabled()) {
-                    mc = model2model_converter(m_model.get());
+                    mc = model2model_converter(m_model_save.get());
                     mc = concat(m_pred_abs.fmc(), mc.get());
                 }
                 break;