fix #3704

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/qe/qe_mbp.cpp

@@ -364,6 +364,7 @@ public:
     void extract_literals(model& model, expr_ref_vector& fmls) {
         expr_ref val(m);
         model_evaluator eval(model);
+        eval.set_expand_array_equalities(true);
         TRACE("qe", tout << fmls << "\n";);
         for (unsigned i = 0; i < fmls.size(); ++i) {
             expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3;

src/sat/sat_lookahead.cpp

@@ -234,9 +234,9 @@ namespace sat {
         for (bool newbies = false; ; newbies = true) {
             sum = init_candidates(level, newbies);
             if (!m_candidates.empty()) break;
-            if (is_sat()) {
+            if (is_sat() || newbies) {
                 return false;
-            }         
+            }                     
         }
         SASSERT(!m_candidates.empty());
         // cut number of candidates down to max_num_cand.
@@ -334,7 +334,7 @@ namespace sat {
                 }                
             }
         }
-        if (m_candidates.empty() && (m_select_lookahead_vars.empty() || newbies)) {
+        if (m_candidates.empty() && (m_select_lookahead_vars.empty() && newbies)) {
             for (bool_var x : m_freevars) {
                 SASSERT(is_undef(x));
                 if (newbies || active_prefix(x)) {
@@ -635,9 +635,7 @@ namespace sat {
             if (sz-- == 0) break;
             tsum += h[b.m_u.index()] * h[b.m_v.index()];
         }
-        // std::cout << "sum: " << sum << " afactor " << afactor << " sqfactor " << sqfactor << " tsum " << tsum << "\n";
         sum = (double)(0.1 + afactor*sum + sqfactor*tsum);
-        // std::cout << "sum: " << sum << " max score " << m_config.m_max_score << "\n";
         return std::min(m_config.m_max_score, sum);
     }
 
@@ -2224,9 +2222,10 @@ namespace sat {
                 for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
                 m_model.reset();
                 init_model();
-                return l_true;
+                return m_freevars.empty() ? l_true : l_undef;
             }
             TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";);
+            SASSERT(vars.empty() || vars.contains(lit.var()));
             ++m_stats.m_decisions;
             push(lit, c_fixed_truth);
             m_cube_state.m_cube.push_back(lit);
@@ -2512,7 +2511,6 @@ namespace sat {
                     }
                 }
             }
-            // std::cout << candidates.size() << " -> " << k << "\n";
             if (k == candidates.size()) break;
             candidates.shrink(k);
             if (k == 0) break;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -384,7 +384,18 @@ public:
         lit2expr.resize(m_solver.num_vars() * 2);
         m_map.mk_inv(lit2expr);
         for (sat::literal l : lits) {
-            fmls.push_back(lit2expr[l.index()].get());
+            expr* e = lit2expr.get(l.index());
+            if (!e) {
+                std::cout << l << "\n";
+                std::cout << lits << "\n";
+                std::cout << vars << "\n";
+                std::cout << lit2expr << "\n";
+                for (auto const& kv : m_map) {
+                    std::cout << kv.m_value << " " << mk_pp(kv.m_key, m) << "\n";
+                }
+            }
+            SASSERT(e);
+            fmls.push_back(e);
         }
         vs.reset();
         for (sat::bool_var v : vars) {

src/solver/parallel_tactic.cpp

@@ -236,7 +236,9 @@ class parallel_tactic : public tactic {
         vector<cube_var> split_cubes(unsigned n) {
             vector<cube_var> result;
             while (n-- > 0 && !m_cubes.empty()) {
+                for (expr* c : m_cubes.back().cube()) SASSERT(c);
                 result.push_back(m_cubes.back());
+
                 m_cubes.pop_back();
             }
             return result;
@@ -244,6 +246,7 @@ class parallel_tactic : public tactic {
 
         void set_cubes(vector<cube_var>& c) {
             m_cubes.reset();
+            for (auto & cb : c) for (expr* e : cb.cube()) SASSERT(e);
             m_cubes.append(c);
         }
 
@@ -454,6 +457,7 @@ private:
         ast_manager& m = s.m();
         vector<cube_var> cube, hard_cubes, cubes;
         expr_ref_vector vars(m);
+        unsigned num_simplifications = 0;
 
     cube_again:
         // extract up to one cube and add it.
@@ -467,8 +471,10 @@ private:
             vars.reset();
             vars.append(cube.get(0).vars());
         }
+        num_simplifications = 0;
 
     simplify_again:
+        ++num_simplifications;
         s.inc_depth(1);
         // simplify
         if (canceled(s)) return;
@@ -493,7 +499,11 @@ private:
         unsigned num_backtracks = 0, width = 0;
         while (cutoff > 0 && !canceled(s)) {
             expr_ref_vector c = s.get_solver().cube(vars, cutoff);
-            if (c.empty()) {
+            if (c.empty() || (cube.size() == 1 && m.is_true(c.back()))) {
+                if (num_simplifications > 1) {
+                    report_undef(s); 
+                    return;
+                }
                 goto simplify_again;
             }
             if (m.is_false(c.back())) {                
@@ -507,6 +517,7 @@ private:
             if (conquer) {
                 is_sat = conquer->check_sat(c);
             }
+            for (expr* e : c) SASSERT(e);
             switch (is_sat) {
             case l_false: 
                 cutoff = c.size();