mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

fix #6670

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-04-08 16:55:23 -07:00
parent ccb250c32b
commit af9c760a68
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_lra.cpp
View file

@ -1314,7 +1314,6 @@ public:
expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m);
expr_ref mone(a.mk_int(-1), m);
expr_ref modmq(a.mk_sub(mod, abs_q), m);
ctx().get_rewriter()(modmq);
literal eqz = mk_literal(m.mk_eq(q, zero));
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
literal mod_lt_q = mk_literal(a.mk_le(modmq, mone));