From 578e24d8c1cb49d35b4aba0e43184b7a4195c786 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 11 Jun 2019 21:32:38 -0700
Subject: [PATCH] bound the size of bit vectors

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/tactic/smtlogics/qfnia_tactic.cpp | 10 +++++-----
 src/test/lp/lp.cpp                    | 12 ++++++------
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 93a284946..87f13ced5 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -78,7 +78,7 @@ static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) {
                  using_params(mk_simplify_tactic(m), pull_ite_p),
                  mk_elim_uncnstr_tactic(m),
                  mk_lia2card_tactic(m), 
-                 mk_card2bv_tactic(m, p_ref),
+			     mk_card2bv_tactic(m, p_ref),
                  skip_if_failed(using_params(mk_cofactor_term_ite_tactic(m), elim_p)));
 }
 
@@ -118,12 +118,12 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
     return and_then(
         mk_report_verbose_tactic("(qfnia-tactic)", 10),
         mk_qfnia_premable(m, p),
-        // or_else(mk_qfnia_sat_solver(m, p),
-        //      try_for(mk_qfnia_smt_solver(m, p), 2000),
-        //     mk_qfnia_nlsat_solver(m, p),
+        or_else(mk_qfnia_sat_solver(m, p),
+             try_for(mk_qfnia_smt_solver(m, p), 2000),
+            mk_qfnia_nlsat_solver(m, p),
         
                 mk_qfnia_smt_solver(m, p))
-        //     )
+            )
         ;
 }
 
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 8fd7d3679..5caad4936 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -53,7 +53,7 @@
 #include "math/lp/square_sparse_matrix_def.h"
 #include "math/lp/lu_def.h"
 #include "math/lp/general_matrix.h"
-#include "math/lp/bound_propagator.h"
+#include "math/lp/lp_bound_propagator.h"
 #include "math/lp/nla_solver.h"
 namespace nla {
 void test_order_lemma();
@@ -69,11 +69,11 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
 namespace lp {
 unsigned seed = 1;
 
-    class my_bound_propagator : public bound_propagator {
-    public:
-        my_bound_propagator(lar_solver & ls): bound_propagator(ls) {}
-        void consume(mpq const& v, lp::constraint_index j) override {}
-    };
+class my_bound_propagator : public lp_bound_propagator {
+public:
+    my_bound_propagator(lar_solver & ls): lp_bound_propagator(ls, nullptr) {}
+    void consume(mpq const& v, lp::constraint_index j) override {}
+};
 
 random_gen g_rand;
 static unsigned my_random() {