diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-05-17 15:33:13 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-05-17 15:33:13 +0000 |
| commit | a6f69a821e2d26f8901662193da5ee8dc74b158a (patch) | |
| tree | d1ecbfdaa551fffa00feca39869d7beae36396bc /test | |
| parent | a998a2a58571f6791b019fe77e698e05ce3fadd2 (diff) | |
Adding failing regression for ite type computation.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/bug339.smt2 | 15 |
2 files changed, 17 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 881664e83..db9b4d07f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -97,7 +97,8 @@ BUG_TESTS = \ bug239.smt \ buggy-ite.smt2 \ bug303.smt2 \ - bug310.cvc + bug310.cvc \ + bug339.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug339.smt2 b/test/regress/regress0/bug339.smt2 new file mode 100644 index 000000000..bb03cf9b1 --- /dev/null +++ b/test/regress/regress0/bug339.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_LRA) +(set-info :status sat) + +(declare-fun x () Real) +(declare-fun P () Bool) + +(assert + (let ((y (ite P 1 x))) + (and (not (= y 1)) + (> y 0) + (<= y 1)))) + +(check-sat) + +(exit) |