diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-12-18 07:01:58 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-18 09:01:58 -0600 |
| commit | 5b05e467710e07bbfa27d4a2417ec27b336c245d (patch) | |
| tree | b909dc2937e88d79a7a631b1afa9caf8fd78df88 /test/regress/regress0/arith | |
| parent | 8a2a526b2dab5d6efaf1435afcc1b7be113a86bf (diff) | |
Bugfix: proofs for props of non-normal arith lits (#5702)
Arith has a normal form for literals, which the rewriter computes.
Nonetheless, arith sometimes gets (and ultimately propagates) non-normal
literals. It normalizes them internally and goes about its business.
However, when asked for an explanation, it must prove the non-normal
literal, rather than the normal one.
Also includes a regression for the bug, courtesy of Andy.
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
Diffstat (limited to 'test/regress/regress0/arith')
| -rw-r--r-- | test/regress/regress0/arith/non-normal.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/non-normal.smt2 b/test/regress/regress0/arith/non-normal.smt2 new file mode 100644 index 000000000..389bd6d2b --- /dev/null +++ b/test/regress/regress0/arith/non-normal.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --proof-new-eager-checking +; EXPECT: sat +(set-logic QF_UFLRA) +(declare-fun v1 () Real) +(declare-fun v2 () Real) +(declare-fun f1 (Real) Real) +(declare-fun f0 (Real Real) Real) +(declare-fun p0 (Real Real) Bool) +(assert +(ite + (or (= 0.0 v2) (> 1 (ite (< (- (- v1)) 1.0) 1.0 (ite (p0 0.0 v1) 0.0 1.0)))) + (= 0.0 (ite (= 1.0 (f1 0.0)) 0.0 (f1 1.0))) + (and + (= 1.0 (ite (= 0.0 (f1 1.0)) v2 (- 1.0))) + (=> (not (p0 0.0 (- (- (- v2))))) (= 1.0 (ite (= 1.0 v2) (ite (= 0 (f0 0.0 1.0)) 1.0 (f0 0.0 (- v2 (- v1)))) 0.0)))))) +(check-sat) |