diff options
Diffstat (limited to 'test/regress/regress0/uflra/constants0.smt')
| -rw-r--r-- | test/regress/regress0/uflra/constants0.smt | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/test/regress/regress0/uflra/constants0.smt b/test/regress/regress0/uflra/constants0.smt deleted file mode 100644 index b07a6bc4e..000000000 --- a/test/regress/regress0/uflra/constants0.smt +++ /dev/null @@ -1,15 +0,0 @@ -(benchmark mathsat -:logic QF_UFLRA -:status unsat -:category { crafted } -:extrafuns ((f Real Real)) -:extrafuns ((x Real)) -:extrafuns ((y Real)) -:formula -(and (or (= x 3) (= x 5)) - (or (= y 3) (= y 5)) - (not (= (f x) (f y))) - (implies (= (f 3) (f x)) (= (f 5) (f x))) - (implies (= (f 3) (f y)) (= (f 5) (f y))) -) -)
\ No newline at end of file |