From 5dd7e2c520b37c75bfe3c22f1e81911373e1dfed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 16 Mar 2018 19:30:13 -0700
Subject: [PATCH] fix #1544

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/z3.h                    |  1 -
 src/ast/rewriter/rewriter_def.h |  2 ++
 src/model/model_evaluator.cpp   | 11 +++++------
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/api/z3.h b/src/api/z3.h
index b29f1d6ba..e08b0c073 100644
--- a/src/api/z3.h
+++ b/src/api/z3.h
@@ -22,7 +22,6 @@ Notes:
 #define Z3_H_
 
 #include <stdio.h>
-#include <stdbool.h>
 #include "z3_macros.h"
 #include "z3_api.h"
 #include "z3_ast_containers.h"
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 878f4ef4c..dfb6542d6 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -194,12 +194,14 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
             result_stack().shrink(fr.m_spos);
             result_stack().push_back(arg);
             fr.m_state = REWRITE_BUILTIN;
+            TRACE("rewriter_step", tout << "step\n" << mk_ismt2_pp(t, m()) << "\n";);
             if (visit<false>(arg, fr.m_max_depth)) {
                 m_r = result_stack().back();
                 result_stack().pop_back();
                 result_stack().pop_back();
                 result_stack().push_back(m_r);
                 cache_result<false>(t, m_r, m_pr, fr.m_cache_result);
+                TRACE("rewriter_step", tout << "step 1\n" << mk_ismt2_pp(m_r, m()) << "\n";);
                 frame_stack().pop_back();
                 set_new_child_flag(t);
             }
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index fd2dc7656..227e14ca6 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -187,14 +187,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
             TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
                   for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
                   tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";);
-            return BR_DONE;
+            return BR_REWRITE1;
         }
         if (st == BR_FAILED && !m.is_builtin_family_id(fid))
             st = evaluate_partial_theory_func(f, num, args, result, result_pr);
         if (st == BR_DONE && is_app(result)) {
             app* a = to_app(result);
             if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
-                return BR_DONE;
+                return BR_REWRITE1;
             }
         }
         CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
@@ -399,12 +399,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 }
             }
         }
-        args_table::iterator it = table1.begin(), end = table1.end();
-        for (; it != end; ++it) {
-            switch (compare((*it)[arity], else2)) {
+        for (auto const& t : table1) {
+            switch (compare((t)[arity], else2)) {
             case l_true: break;
             case l_false: result = m.mk_false(); return BR_DONE;
-            default: conj.push_back(m.mk_eq((*it)[arity], else2)); break;
+            default: conj.push_back(m.mk_eq((t)[arity], else2)); break;
             }
         }
         result = mk_and(conj);