mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b352d43e50
commit
30f8110488
|
@ -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());
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue