Added missing decide-callback for tactics (#6166)

* Added function to select the next variable to split on * Fixed typo * Small fixes * uint -> int * Fixed missing assignment for binary clauses * Added missing decide-callback for tactics
Z3Prover · Jul 17, 2022 · 95c3dd9 · 95c3dd9
1 parent 6e5ced0
commit 95c3dd9
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
@@ -348,6 +348,7 @@ class smt_tactic : public tactic {
         m_eq_eh = nullptr;
         m_diseq_eh = nullptr;
         m_created_eh = nullptr;
+        m_decide_eh = nullptr;
     }
 
     void user_propagate_init(
@@ -385,6 +386,10 @@ class smt_tactic : public tactic {
     void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override {
         m_created_eh = created_eh;
     }
+
+    void user_propagate_register_decide(user_propagator::decide_eh_t& decide_eh) override {
+        m_decide_eh = decide_eh;
+    }
 };
 
 static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) {

diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
@@ -116,8 +116,8 @@ class tactic2solver : public solver_na2as {
         m_tactic->user_propagate_register_created(created_eh);
     }
 
-    void user_propagate_register_decide(user_propagator::decide_eh_t& created_eh) override {
-        m_tactic->user_propagate_register_decide(created_eh);
+    void user_propagate_register_decide(user_propagator::decide_eh_t& decide_eh) override {
+        m_tactic->user_propagate_register_decide(decide_eh);
     }
 
     void user_propagate_clear() override {