From 49483fdc28292789c60b267475aae2b0fa40a170 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 21 Feb 2015 02:08:00 -0800
Subject: [PATCH] take conflicts during restart into account. reported by Arie
 Gurfinkel

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .../simplifier/array_simplifier_plugin.cpp    | 29 +++++++++++++------
 src/smt/arith_eq_adapter.cpp                  |  3 +-
 src/smt/smt_context.cpp                       | 11 +++++--
 3 files changed, 31 insertions(+), 12 deletions(-)

diff --git a/src/ast/simplifier/array_simplifier_plugin.cpp b/src/ast/simplifier/array_simplifier_plugin.cpp
index 065f8bd96..0a8aefa93 100644
--- a/src/ast/simplifier/array_simplifier_plugin.cpp
+++ b/src/ast/simplifier/array_simplifier_plugin.cpp
@@ -327,16 +327,20 @@ void array_simplifier_plugin::get_stores(expr* n, unsigned& arity, expr*& m, ptr
 }
 
 lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st) {
+    bool all_diseq = m_manager.is_unique_value(def) && num_st > 0;
+    bool all_eq = true;
     for (unsigned i = 0; i < num_st; ++i) {
-        if (st[i][arity] == def) {
-            continue;
-        }
-        if (m_manager.is_unique_value(st[i][arity]) && m_manager.is_unique_value(def)) {
-            return l_false;
-        }
-        return l_undef;
+        all_eq  &= (st[i][arity] == def);
+        all_diseq &= m_manager.is_unique_value(st[i][arity]) && (st[i][arity] != def);
+        TRACE("array_simplifier", tout << m_manager.is_unique_value(st[i][arity]) << " " << mk_pp(st[i][arity], m_manager) << "\n";);
     }
-    return l_true;
+    if (all_eq) {
+        return l_true;
+    }
+    if (all_diseq) {
+        return l_false;
+    }   
+    return l_undef;
 }
 
 bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) {
@@ -346,6 +350,12 @@ bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned n
                 return false;
             }
         }
+        TRACE("array_simplifier", tout << "inserting: ";
+              for (unsigned j = 0; j < arity; ++j) {
+                  tout << mk_pp(st[i][j], m_manager) << " ";              
+              }
+            tout << " |-> " << mk_pp(def, m_manager) << "\n";
+            );
         args_entry e(arity, st[i]);
         table.insert_if_not_there(e);
     }
@@ -419,7 +429,8 @@ bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & resul
             lbool eq = eq_stores(c1, arity, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr());
             TRACE("array_simplifier", 
                   tout << mk_pp(lhs, m_manager) << " = " 
-                  << mk_pp(rhs, m_manager) << " := " << eq << "\n";);
+                  << mk_pp(rhs, m_manager) << " := " << eq << "\n";
+                  tout << "arity: " << arity << "\n";);
             switch(eq) {
             case l_false: 
                 result = m_manager.mk_false(); 
diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp
index 53227d0cc..74e3d573a 100644
--- a/src/smt/arith_eq_adapter.cpp
+++ b/src/smt/arith_eq_adapter.cpp
@@ -287,12 +287,13 @@ namespace smt {
     }
 
     void arith_eq_adapter::restart_eh() { 
+        context & ctx = get_context();
         TRACE("arith_eq_adapter", tout << "restart\n";);
         svector<enode_pair> tmp(m_restart_pairs);
         svector<enode_pair>::iterator it  =  tmp.begin();
         svector<enode_pair>::iterator end =  tmp.end();
         m_restart_pairs.reset();
-        for (; it != end; ++it) {
+        for (; it != end && !ctx.inconsistent(); ++it) {
             TRACE("arith_eq_adapter", tout << "creating arith_eq_adapter axioms at the base level #" << it->first->get_owner_id() << " #" <<
                   it->second->get_owner_id() << "\n";);
             mk_axioms(it->first, it->second);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index adb17f6e2..f5d99325b 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3236,10 +3236,17 @@ namespace smt {
                 }
                 ptr_vector<theory>::iterator it  = m_theory_set.begin();
                 ptr_vector<theory>::iterator end = m_theory_set.end();
-                for (; it != end; ++it)
+                for (; it != end && !inconsistent(); ++it)
                     (*it)->restart_eh();
                 TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";); 
-                m_qmanager->restart_eh();                
+                if (!inconsistent()) {
+                    m_qmanager->restart_eh();                
+                }
+                if (inconsistent()) {
+                    VERIFY(!resolve_conflict());
+                    status = l_false;      
+                    break;
+                }
             }
             if (m_fparams.m_simplify_clauses)
                 simplify_clauses();