From 145ec8f248dae5b6cff03a3d0be3e1589cdb340b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Mar 2020 10:51:55 -0700
Subject: [PATCH] pick up log configuration consistently #3513

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_solver.cpp              | 20 ++++++++++++++++----
 src/ast/rewriter/arith_rewriter.cpp |  2 +-
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 4d4d52926..a512d7a46 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -151,6 +151,14 @@ extern "C" {
             init_solver_core(c, s);
     }
 
+    static void init_solver_log(Z3_context c, Z3_solver s) {
+        solver_params sp(to_solver(s)->m_params);
+        symbol smt2log = sp.smtlib2_log();
+        if (smt2log.is_non_empty_string() && !to_solver(s)->m_pp) {
+            to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str().c_str());
+        }
+    }
+
     Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c) {
         Z3_TRY;
         LOG_Z3_mk_simple_solver(c);
@@ -158,6 +166,7 @@ extern "C" {
         Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_solver_factory());
         mk_c(c)->save_object(s);
         Z3_solver r = of_solver(s);
+        init_solver_log(c, r);
         RETURN_Z3(r);
         Z3_CATCH_RETURN(nullptr);
     }
@@ -169,6 +178,7 @@ extern "C" {
         Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory());
         mk_c(c)->save_object(s);
         Z3_solver r = of_solver(s);
+        init_solver_log(c, r);
         RETURN_Z3(r);
         Z3_CATCH_RETURN(nullptr);
     }
@@ -187,6 +197,7 @@ extern "C" {
             Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory(to_symbol(logic)));
             mk_c(c)->save_object(s);
             Z3_solver r = of_solver(s);
+            init_solver_log(c, r);
             RETURN_Z3(r);
         }
         Z3_CATCH_RETURN(nullptr);
@@ -199,6 +210,7 @@ extern "C" {
         Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_tactic2solver_factory(to_tactic_ref(t)));
         mk_c(c)->save_object(s);
         Z3_solver r = of_solver(s);
+        init_solver_log(c, r);
         RETURN_Z3(r);
         Z3_CATCH_RETURN(nullptr);
     }
@@ -213,6 +225,7 @@ extern "C" {
         sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
         mk_c(target)->save_object(sr);
         Z3_solver r = of_solver(sr);
+        init_solver_log(target, r);
         RETURN_Z3(r);
         Z3_CATCH_RETURN(nullptr);
     }
@@ -343,19 +356,16 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+
     void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p) {
         Z3_TRY;
         LOG_Z3_solver_set_params(c, s, p);
         RESET_ERROR_CODE();
 
         symbol logic = to_param_ref(p).get_sym("smt.logic", symbol::null);
-        symbol smt2log = to_param_ref(p).get_sym("solver.smtlib2_log", symbol::null);
         if (logic != symbol::null) {
             to_solver(s)->m_logic = logic;
         }
-        if (smt2log != symbol::null && !to_solver(s)->m_pp) {
-            to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str().c_str());
-        }
         if (to_solver(s)->m_solver) {
             bool old_model = to_solver(s)->m_params.get_bool("model", true);
             bool new_model = to_param_ref(p).get_bool("model", true);
@@ -368,6 +378,8 @@ extern "C" {
             to_solver_ref(s)->updt_params(to_param_ref(p));
         }
         to_solver(s)->m_params.append(to_param_ref(p));
+
+        init_solver_log(c, s);
         
         Z3_CATCH;
     }
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 732bde404..0126c1e16 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -190,7 +190,7 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref &
             case EQ: result = m().mk_false(); return true;
             }
         }
-        expr * k = m_util.mk_numeral(c, is_int);
+        expr_ref k(m_util.mk_numeral(c, is_int), m());
         switch (kind) {
         case LE: result = m_util.mk_le(pp, k); return true;
         case GE: result = m_util.mk_ge(pp, k); return true;