diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-09 21:05:43 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-09 21:05:43 +0000 |
| commit | fc163356c3bcc6e21bbb52e0e7de719817138eb7 (patch) | |
| tree | 0e0d202f83f65843c9fa41bda60430c36787e17e | |
| parent | 3cc7c610a84a29f97a206227d85efbb9a77fda9f (diff) | |
Test that breaks arithmetic model building due to disequality terms.
| -rw-r--r-- | test/regress/regress0/uflra/neq-deltacomp.smt | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/uflra/neq-deltacomp.smt b/test/regress/regress0/uflra/neq-deltacomp.smt new file mode 100644 index 000000000..4144fcb79 --- /dev/null +++ b/test/regress/regress0/uflra/neq-deltacomp.smt @@ -0,0 +1,14 @@ +(benchmark fuzzsmt +:logic QF_UFLRA +:extrafuns ((v2 Real)) +:extrafuns ((v1 Real)) +:extrafuns ((v0 Real)) +:status unknown +:formula +(let (?n1 (~ v1)) +(flet ($n2 (>= ?n1 v0)) +(let (?n3 1) +(let (?n4 (ite $n2 v1 ?n3)) +(flet ($n5 (<= ?n4 v2)) +$n5 +)))))) |