mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-19 13:13:09 -07:00
parent af2f74c05f
commit 72d129eb75
1 changed files with 2 additions and 1 deletions

3
src/smt/arith_eq_adapter.cpp
View file

@ -81,7 +81,8 @@ namespace smt {
};
void arith_eq_adapter::mk_axioms(enode * n1, enode * n2) {
SASSERT(n1 != n2);
if (n1 == n2)
return;
ast_manager & m = get_manager();
TRACE("arith_eq_adapter_mk_axioms", tout << "#" << n1->get_owner_id() << " #" << n2->get_owner_id() << "\n";
tout << mk_ismt2_pp(n1->get_owner(), m) << "\n" << mk_ismt2_pp(n2->get_owner(), m) << "\n";);