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 | |
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')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/arith/non-normal.smt2 | 16 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d185049e0..2c480da3a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -68,6 +68,7 @@ set(regress_0_tests regress0/arith/mod-simp.smt2 regress0/arith/mod.01.smt2 regress0/arith/mult.01.smt2 + regress0/arith/non-normal.smt2 regress0/arr1.smt2 regress0/arr1.smtv1.smt2 regress0/arr2.smtv1.smt2 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) |