diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-10 21:48:13 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-10 20:48:13 +0000 |
| commit | bd52deb7434b1b08a122db4513972644c11fc4aa (patch) | |
| tree | 44cd11cde22fe7f20a281c8d9092de219547c6fb /src/expr/expr_manager_template.cpp | |
| parent | 27fb04bc96999e101b45458c549345e864e085e9 (diff) | |
Improve arithmetic proofs (#6106)
The proof rules for ARITH_MULT_POS and ARITH_MULT_NEG were complex than necessary in that they incorporated a rewriting step. This PR removes rewriting from these rules, making them cleaner and easier to understand.
The proof now applies these simpler rule and uses MACRO_SR_PRED_TRANSFORM to prove the lemma that is actually added.
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
0 files changed, 0 insertions, 0 deletions