diff options
Diffstat (limited to 'test/regress/regress0/uflra/constants0.smt')
-rw-r--r-- | test/regress/regress0/uflra/constants0.smt | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/test/regress/regress0/uflra/constants0.smt b/test/regress/regress0/uflra/constants0.smt deleted file mode 100644 index 87d762e54..000000000 --- a/test/regress/regress0/uflra/constants0.smt +++ /dev/null @@ -1,16 +0,0 @@ -; COMMAND-LINE: --no-check-proofs -(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))) -) -) |