From fde64365a30ce6be70ab98fa8cc221cef841c9aa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 13 Dec 2023 14:13:16 -0800
Subject: [PATCH] bugfixes in intblast solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/arith_solver.cpp    |  3 +++
 src/sat/smt/intblast_solver.cpp |  1 -
 src/sat/smt/intblast_solver.h   | 11 +++++++----
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 078515184..6f08fe6a1 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -628,6 +628,9 @@ namespace arith {
         }
         else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) {
             anum const& an = nl_value(v, m_nla->tmp1());
+
+
+
             if (a.is_int(o) && !m_nla->am().is_int(an))
                 value = a.mk_numeral(rational::zero(), a.is_int(o));
             else
diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 9f0541122..99a96b374 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -233,7 +233,6 @@ namespace intblast {
         }
 
         m_core.reset();
-        m_translate.reset();
         m_is_plugin = false;
         m_solver = mk_smt2_solver(m, s.params(), symbol::null);
 
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index 2c0ebda28..e6f82f7cf 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -54,6 +54,7 @@ namespace intblast {
         scoped_ptr<::solver> m_solver;
         obj_map<func_decl, func_decl*> m_new_funs;
         expr_ref_vector m_translate, m_args;
+        ast_ref_vector m_pinned;
         sat::literal_vector m_core;
         ptr_vector<app> m_bv2int, m_int2bv;
         statistics m_stats;
@@ -94,8 +95,9 @@ namespace intblast {
         void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values);
         void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values);
 
+        bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); }
         expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
-        void set_translated(expr* e, expr* r) { SASSERT(r); m_translate.setx(e->get_id(), r); }
+        void set_translated(expr* e, expr* r);
         expr* arg(unsigned i) { return m_args.get(i); }
 
         expr* umod(expr* bv_expr, unsigned i);
@@ -112,9 +114,10 @@ namespace intblast {
         void ensure_translated(expr* e);
         void internalize_bv(app* e);
 
-        unsigned m_vars_qhead = 0;
-        ptr_vector<expr> m_vars;
-        void add_bound_axioms();
+        unsigned m_vars_qhead = 0, m_preds_qhead = 0;
+        ptr_vector<expr> m_vars, m_preds;
+        bool add_bound_axioms();
+        bool add_predicate_axioms();
 
         euf::theory_var mk_var(euf::enode* n) override;