Skip to content

Commit

Permalink
for Arie
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jun 11, 2022
1 parent 994dab8 commit 9cd3398
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/ast/rewriter/arith_rewriter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -729,7 +729,9 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
expr_ref arith_rewriter::neg_monomial(expr* e) const {
expr_ref_vector args(m());
rational a1;
if (is_app(e) && m_util.is_mul(e)) {
if (m_util.is_numeral(e, a1))
args.push_back(m_util.mk_numeral(-a1, e->get_sort()));
else if (is_app(e) && m_util.is_mul(e)) {
if (is_numeral(to_app(e)->get_arg(0), a1)) {
if (!a1.is_minus_one()) {
args.push_back(m_util.mk_numeral(-a1, m_util.is_int(e)));
Expand Down

1 comment on commit 9cd3398

@NikolajBjorner
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm running into a problem that arith_rewriteris not idempotent.
It rewrites t <= c into -t >= -c and t >=c into -t <= -c

The source is this line:
https://github.com/Z3Prover/z3/blob/master/src/ast/rewriter/arith_rewriter.cpp#L649

I don't understand why this is done. I do what arith_lhs, but I don't see how this helps with that.

arie

Please sign in to comment.