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

fix #6194

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-27 08:03:57 +02:00
parent b6c80e8b00
commit 8551b217ce
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_lra.cpp
View file

@ -1113,7 +1113,7 @@ public:
} }
{ {
scoped_trace_stream ts(th, dgez, neg); scoped_trace_stream ts(th, dgez, neg);
mk_axiom( dgez, neg); mk_axiom( dgez, neg);
} }
} }
@ -1224,7 +1224,6 @@ public:
return; return;
} }
expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m); expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m);
ctx().get_rewriter()(mod_r);
expr_ref eq_r(th.mk_eq_atom(mod_r, p), m); expr_ref eq_r(th.mk_eq_atom(mod_r, p), m);
ctx().internalize(eq_r, false); ctx().internalize(eq_r, false);
literal eq = ctx().get_literal(eq_r); literal eq = ctx().get_literal(eq_r);