mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 21:31:22 +00:00
Code Activity

fix perf regression for new solver, missing equality propagations #5106

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-28 14:14:25 -07:00
parent bb2c40072e
commit d6691830c7
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_lra.cpp
View file

@ -570,7 +570,6 @@ class theory_lra::imp {
} }
void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) { void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
TRACE("arith", literal lits[3]; lits[0] = l1; lits[1] = l2; lits[2] = l3; ctx().display_literals_verbose(tout, 3, lits); tout << "\n";);
ctx().mk_th_axiom(get_id(), l1, l2, l3, num_params, params); ctx().mk_th_axiom(get_id(), l1, l2, l3, num_params, params);
} }