From 95c3dd9224b538b940dbb9d91f0ae7d42f3f70d5 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Sun, 17 Jul 2022 19:07:52 +0200
Subject: [PATCH] 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
---
 src/smt/tactic/smt_tactic_core.cpp | 5 +++++
 src/solver/tactic2solver.cpp       | 4 ++--
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index 9c5fc1c8e..c45165d79 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -348,6 +348,7 @@ public:
         m_eq_eh = nullptr;
         m_diseq_eh = nullptr;
         m_created_eh = nullptr;
+        m_decide_eh = nullptr;
     }
 
     void user_propagate_init(
@@ -385,6 +386,10 @@ public:
     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
index fe89d6533..09ede0c35 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -116,8 +116,8 @@ public:
         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 {