From f4c500c5197f559870e1fd78bd52496024493c4e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 16 Apr 2022 15:16:53 +0200
Subject: [PATCH] fix build

reference types are not part of C
---
 src/api/api_solver.cpp             |  2 +-
 src/api/z3_api.h                   |  2 +-
 src/opt/maxres.cpp                 | 11 ++++++++---
 src/smt/theory_user_propagator.cpp |  2 +-
 src/tactic/user_propagator_base.h  |  2 +-
 5 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index a0803516f..05b125546 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -978,7 +978,7 @@ extern "C" {
     void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh) {
         Z3_TRY;
         RESET_ERROR_CODE();
-        user_propagator::decide_eh_t c = (void(*)(void*, user_propagator::callback*, expr*&, unsigned&, lbool&))decide_eh;
+        user_propagator::decide_eh_t c = (void(*)(void*, user_propagator::callback*, expr**, unsigned*, lbool*))decide_eh;
         to_solver_ref(s)->user_propagate_register_decide(c);
         Z3_CATCH;
     }
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 1eb2164d5..2680b6f82 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1444,7 +1444,7 @@ Z3_DECLARE_CLOSURE(Z3_fixed_eh,   void, (void* ctx, Z3_solver_callback cb, Z3_as
 Z3_DECLARE_CLOSURE(Z3_eq_eh,      void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t));
 Z3_DECLARE_CLOSURE(Z3_final_eh,   void, (void* ctx, Z3_solver_callback cb));
 Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t));
-Z3_DECLARE_CLOSURE(Z3_decide_eh,  void, (void* ctx, Z3_solver_callback cb, Z3_ast&, unsigned&, Z3_lbool&));
+Z3_DECLARE_CLOSURE(Z3_decide_eh,  void, (void* ctx, Z3_solver_callback cb, Z3_ast*, unsigned*, Z3_lbool*));
 
 
 /**
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index d316f9360..4c9964cf4 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -700,7 +700,7 @@ public:
         }
     }
 
-#if 0
+#if 1
 
     void bin_max_resolve(exprs const& _core, rational const& w) {
         expr_ref_vector core(m, _core.size(), _core.data());
@@ -708,8 +708,8 @@ public:
         for (unsigned i = 0; i + 1 < core.size(); ++i) {
             expr* a = core.get(i);
             expr* b = core.get(i + 1);
-            expr_ref u = mk_fresh_bool("u");
-            expr_ref v = mk_fresh_bool("v");
+            expr* u = mk_fresh_bool("u");
+            expr* v = mk_fresh_bool("v");
             // u = a or b
             // v = a and b
             cls = m.mk_or(a, b);
@@ -725,8 +725,13 @@ public:
             new_assumption(u, w);
             core.push_back(v);
         }
+        s().assert_expr(m.mk_not(core.back()));
     }
 
+#endif
+
+#if 0
+
     struct unfold_record {
         ptr_vector<expr> ws;
         rational weight;
diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index bf8722701..1b0cc429d 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -190,7 +190,7 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
     lbool phase = is_pos ? l_true : l_false;
 
     expr* e = var2expr(original_enode->get_th_var(get_family_id()));
-    m_decide_eh(m_user_context, this, e, new_bit, phase);
+    m_decide_eh(m_user_context, this, &e, &new_bit, &phase);
     enode* new_enode = ctx.get_enode(e);
 
     // check if the callback changed something
diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h
index c67a073cd..3f4af0329 100644
--- a/src/tactic/user_propagator_base.h
+++ b/src/tactic/user_propagator_base.h
@@ -25,7 +25,7 @@ namespace user_propagator {
     typedef std::function<void(void*, callback*)>                            push_eh_t;
     typedef std::function<void(void*, callback*, unsigned)>                  pop_eh_t;
     typedef std::function<void(void*, callback*, expr*)>                     created_eh_t;
-    typedef std::function<void(void*, callback*, expr*&, unsigned&, lbool&)> decide_eh_t;
+    typedef std::function<void(void*, callback*, expr**, unsigned*, lbool*)> decide_eh_t;
 
     class plugin : public decl_plugin {
     public: