fixes to lazy tactic uses

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 27, 2024 · 40b0210 · 40b0210
1 parent 01cf042
commit 40b0210
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp
@@ -89,7 +89,7 @@ tactic * mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) {
         p_i.set_bool("shuffle_vars", true);
         // if ((i & 1) == 0)
         //     p_i.set_bool("randomize", false);
-        ts.push_back(mk_lazy_tactic(m, p_i, [&](ast_manager& m, params_ref const& p) { return try_for(mk_qfnra_nlsat_tactic(m, p_i), 3 * 1000); }));
+        ts.push_back(mk_lazy_tactic(m, p_i, [&](ast_manager& m, params_ref const& p) { return try_for(mk_qfnra_nlsat_tactic(m, p), 3 * 1000); }));
     }
     {
         ts.push_back(mk_qfnra_nlsat_tactic(m, p));
@@ -147,7 +147,7 @@ tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) {
         p_i.set_bool("shuffle_vars", true);
         // if ((i & 1) == 0)
         //     p_i.set_bool("randomize", false);
-        ts.push_back(mk_lazy_tactic(m, p_i, [&](ast_manager& m, params_ref const& p) { return try_for(mk_qfnra_nlsat_tactic(m, p_i), 5 * 1000); }));
+        ts.push_back(mk_lazy_tactic(m, p_i, [&](ast_manager& m, params_ref const& p) { return try_for(mk_qfnra_nlsat_tactic(m, p), 5 * 1000); }));
     }
     {
         ts.push_back(mk_qfnra_nlsat_tactic(m, p));

diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
@@ -114,6 +114,11 @@ class lazy_tactic : public tactic {
     void user_propagate_initialize_value(expr* var, expr* value) override { if (m_tactic) m_tactic->user_propagate_initialize_value(var, value); }
     tactic* translate(ast_manager& m) override { ensure_tactic(); return m_tactic->translate(m); }
     void reset() override { if (m_tactic) m_tactic->reset(); }
+    void reset_statistics() override { if (m_tactic) m_tactic->reset_statistics(); }
+    void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override {
+        ensure_tactic();
+        m_tactic->register_on_clause(ctx, on_clause);
+    }
 };