diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-10-28 04:01:28 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-10-28 04:01:28 -0700 |
| commit | bab652d9fa2b2efac07b3b686cff3f67b5ef5fda (patch) | |
| tree | a46e22bfa4d068b7f241bf86e06846450d7b699d | |
| parent | 46f5a39730ebd42421963c23de81a75652fb6629 (diff) | |
[FP] Fix overly restrictive assertionprojIssue327
Fixes https://github.com/cvc5/cvc5-projects/issues/327. When generating
refinement lemmas, we were asserting that the concrete value of
conversion from real to a floating-point number was either normal or
subnormal. However, it can also be zero. This commit fixes the assertion
and adds a modified version of the regression that triggers the same
error and terminates quickly with the fix.
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 5 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/fp/proj-issue327-abs-ref-cond.smt2 | 6 |
3 files changed, 10 insertions, 2 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 8364aa81b..36dfbc2b6 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -213,9 +213,10 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) if (abstractValue != concreteValue) { // Need refinement lemmas - // only in the normal and subnormal case + // only in the normal, subnormal, and zero cases Assert(floatValue.getConst<FloatingPoint>().isNormal() - || floatValue.getConst<FloatingPoint>().isSubnormal()); + || floatValue.getConst<FloatingPoint>().isSubnormal() + || floatValue.getConst<FloatingPoint>().isZero()); Node defined = nm->mkNode( kind::AND, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2529a8622..7fb70f936 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1653,6 +1653,7 @@ set(regress_1_tests regress1/decision/wishue160.smt2 regress1/errorcrash.smt2 regress1/fp/fp_to_real.smt2 + regress1/fp/proj-issue327-abs-ref-cond.smt2 regress1/fp/rti_3_5_bug_report.smt2 regress1/fmf-fun-dbu.smt2 regress1/fmf/ALG008-1.smt2 diff --git a/test/regress/regress1/fp/proj-issue327-abs-ref-cond.smt2 b/test/regress/regress1/fp/proj-issue327-abs-ref-cond.smt2 new file mode 100644 index 000000000..76aabeebf --- /dev/null +++ b/test/regress/regress1/fp/proj-issue327-abs-ref-cond.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(declare-const x Real) +(declare-const x6 RoundingMode) +(assert (or (= x (/ 1 1000000000000000000000000000000000000000000000000000000)) (= x 1.0))) +(set-info :status unsat) +(check-sat-assuming ((and (> x 0.0) (> 0.0 (fp.to_real ((_ to_fp 8 24) x6 x)))))) |