mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix tmp_eq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-28 14:28:41 -07:00
parent 67ae75bac7
commit 137e5c5263
1 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/euf/euf_egraph.cpp
View file

@ -722,10 +722,6 @@ namespace euf {
return sat::null_bool_var; return sat::null_bool_var;
} }
enode* r = tmp_eq(ra, rb); enode* r = tmp_eq(ra, rb);
if (!r) {
std::cout << bpp(a) << " " << bpp(b) << "\n";
display(std::cout);
}
SASSERT(r && r->get_root()->value() == l_false); SASSERT(r && r->get_root()->value() == l_false);
explain_eq(justifications, r, r->get_root()); explain_eq(justifications, r, r->get_root());
return r->get_root()->bool_var(); return r->get_root()->bool_var();