From b352d43e50ab214274717fa4968d716d444b807b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 28 Jan 2016 08:50:13 -0800
Subject: [PATCH] fix bugs exposed by Chris' sequence unit tests. Improve
 diagnostics for reason-unknown in combined solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp                | 1 +
 src/smt/theory_seq.cpp         | 8 +++++++-
 src/solver/combined_solver.cpp | 9 +++------
 3 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index a74ab90c1..954f0a85a 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1048,6 +1048,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
         return s2;
     }
     std::ostringstream buffer;
+    SASSERT(false);
     buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
     throw ast_exception(buffer.str().c_str());
 }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index f4e6d1d57..e286add3f 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -584,6 +584,9 @@ bool theory_seq::check_extensionality() {
             for (unsigned i = 0; i < seqs.size(); ++i) {
                 enode* n2 = get_enode(seqs[i]);
                 expr* o2 = n2->get_owner();
+				if (m.get_sort(o1) != m.get_sort(o2)) {
+					continue;
+				}
                 if (m_exclude.contains(o1, o2)) {
                     continue;
                 }
@@ -720,6 +723,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
     context& ctx = get_context();
     expr_ref_vector lhs(m), rhs(m);
     bool changed = false;
+    TRACE("seq", tout << ls << " = " << rs << "\n";);
     if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, changed)) {
         // equality is inconsistent.
         TRACE("seq", tout << ls << " != " << rs << "\n";);
@@ -739,7 +743,6 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
         expr_ref li(lhs[i].get(), m);
         expr_ref ri(rhs[i].get(), m);
         if (solve_unit_eq(li, ri, deps)) {
-            // skip
         }
         else if (m_util.is_seq(li) || m_util.is_re(li)) {
             m_eqs.push_back(mk_eqdep(li, ri, deps));
@@ -1534,6 +1537,9 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
     else if (m_util.str.is_contains(e, e1, e2)) {
         result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps));
     }
+    else if (m_util.str.is_unit(e, e1)) {
+        result = m_util.str.mk_unit(expand(e1, deps));
+    }
     else {
         result = e;
     }
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 08463cf20..338a4a7da 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -190,14 +190,14 @@ public:
     }
 
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
-        m_check_sat_executed  = true;
-        
+        m_check_sat_executed  = true;        
+        m_use_solver1_results = false;
+
         if (get_num_assumptions() != 0 ||            
             num_assumptions > 0 || // assumptions were provided
             m_ignore_solver1)  {
             // must use incremental solver
             switch_inc_mode();
-            m_use_solver1_results = false;
             return m_solver2->check_sat(num_assumptions, assumptions);
         }
         
@@ -206,7 +206,6 @@ public:
                 IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);            
                 lbool r = m_solver2->check_sat(0, 0);
                 if (r != l_undef || !use_solver1_when_undef()) {
-                    m_use_solver1_results = false;
                     return r;
                 }
             }
@@ -219,7 +218,6 @@ public:
                     r = m_solver2->check_sat(0, 0);
                 }
                 if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) {
-                    m_use_solver1_results = false;
                     return r;
                 }
                 if (eh.m_canceled) {
@@ -227,7 +225,6 @@ public:
                 }
             }
             IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);
-
         }
         
         IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";);