From 19fed09122a07cf177361d7012fc0682849e6374 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Feb 2023 08:35:23 -0800
Subject: [PATCH] protecting add_simplifier API against mis-use

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_solver.cpp  | 34 ++++++++++++++++++++++++++++------
 src/api/python/z3/z3.py |  2 --
 2 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 0a3b35aed6b..ca39329bbe4 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -233,16 +233,38 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    /**
+    * attach a simplifier to solver.
+    * This is legal when the solver is fresh, does not already have assertions (and scopes).
+    * To allow recycling the argument solver, we create a fresh copy of it and pass it to 
+    * mk_simplifier_solver.
+    */
     Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier) {
         Z3_TRY;
         LOG_Z3_solver_add_simplifier(c, solver, simplifier); 
-        init_solver(c, solver);
+        solver_ref s_fresh;
+        if (to_solver(solver)->m_solver) {
+            s_fresh = to_solver_ref(solver)->translate(mk_c(c)->m(), to_solver(solver)->m_params);
+        }
+        else {
+            // create the solver, but hijack it for internal uses.
+            init_solver(c, solver);
+            s_fresh = to_solver(solver)->m_solver;
+            to_solver(solver)->m_solver = nullptr;
+        }
+        if (!s_fresh) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, "unexpected empty solver state");
+            RETURN_Z3(nullptr);
+        }
+        if (s_fresh->get_num_assertions() > 0) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, "adding a simplifier to a solver with assertions is not allowed.");
+            RETURN_Z3(nullptr);
+        }        
         auto simp = to_simplifier_ref(simplifier);
-        auto* slv = mk_simplifier_solver(to_solver_ref(solver), simp);
-        Z3_solver_ref* sr = alloc(Z3_solver_ref, *mk_c(c), slv);
-        mk_c(c)->save_object(sr);
-        // ?? init_solver_log(c, sr)
-        RETURN_Z3(of_solver(sr));
+        auto* simplifier_solver = mk_simplifier_solver(s_fresh.get(), simp);
+        Z3_solver_ref* result = alloc(Z3_solver_ref, *mk_c(c), simplifier_solver);
+        mk_c(c)->save_object(result);
+        RETURN_Z3(of_solver(result));
         Z3_CATCH_RETURN(nullptr);
     }
 
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 0f7ef89990c..5cb84723003 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8214,8 +8214,6 @@ def using_params(self, *args, **keys):
 
     def add(self, solver):
         """Return a solver that applies the simplification pre-processing specified by the simplifier"""
-        print(solver.solver)
-        print(self.simplifier)
         return Solver(Z3_solver_add_simplifier(self.ctx.ref(), solver.solver, self.simplifier), self.ctx)
 
     def help(self):