diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-14 22:43:57 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-14 22:43:57 +0000 |
| commit | aa4b06d4f1db1942d7ad3833e071baa356cefd60 (patch) | |
| tree | a05375bd9766663f5e095c91e016464ce16ed413 /test/regress/regress0/uflra | |
| parent | 56013a80a76b0d46f6f8497d7570e51877dbf99d (diff) | |
Fix to bug449. Adds shared constants to the set of DeltaRationals that must be in the final total order.
Diffstat (limited to 'test/regress/regress0/uflra')
| -rw-r--r-- | test/regress/regress0/uflra/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/bug449.smt | 11 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 86a1a9431..352161466 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -23,6 +23,7 @@ SMT_TESTS = \ simple.03.cvc \ simple.04.cvc \ bug293.cvc \ + bug449.smt \ pb_real_10_0100_10_10.smt \ pb_real_10_0100_10_11.smt \ pb_real_10_0100_10_15.smt \ diff --git a/test/regress/regress0/uflra/bug449.smt b/test/regress/regress0/uflra/bug449.smt new file mode 100644 index 000000000..91bb5fb48 --- /dev/null +++ b/test/regress/regress0/uflra/bug449.smt @@ -0,0 +1,11 @@ +(benchmark fuzzsmt +:logic QF_UFLRA +:extrapreds ((p0 Real)) +:extrafuns ((v0 Real)) +:status sat +:formula +(and + (p0 v0) + (< v0 0) + (not (p0 (- 1))) +)) |