From cd8b317b498c6c383c7571cd0939ff5044ad8932 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Fri, 4 Jun 2010 17:14:04 +0000 Subject: Enabling RDL/IDL in SMT v1 and adding some simple tests --- test/regress/regress0/simple-rdl.smt2 | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test/regress/regress0/simple-rdl.smt2 (limited to 'test/regress/regress0/simple-rdl.smt2') diff --git a/test/regress/regress0/simple-rdl.smt2 b/test/regress/regress0/simple-rdl.smt2 new file mode 100644 index 000000000..d2c0a4cde --- /dev/null +++ b/test/regress/regress0/simple-rdl.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_RDL) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (not (=> (< (- x y) 0) (< x y)))) +(check-sat) + -- cgit v1.2.3