mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d5dfe07203
commit
d22ad5e819
|
@ -1702,7 +1702,6 @@ public:
|
|||
is_eq(v1, v2) && n1->get_root() != n2->get_root(),
|
||||
tout << "assuming eq: v" << v1 << " = v" << v2 << "\n";);
|
||||
if (is_eq(v1, v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) {
|
||||
std::cout << v1 << " == " << v2 << "\n"; // mk_pp(n1->get_owner(), m) << " == " << mk_pp(n2->get_owner(), m) << "\n";
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue