From 30f8110488e835f09833366ffe274541135e7217 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Jan 2016 08:51:04 -0800 Subject: [PATCH] fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 - src/smt/theory_seq.cpp | 6 +++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 954f0a85a..a74ab90c1 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1048,7 +1048,6 @@ 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 e286add3f..5472583ff 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -584,9 +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.get_sort(o1) != m.get_sort(o2)) { + continue; + } if (m_exclude.contains(o1, o2)) { continue; }