diff options
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/Makefile.am | 8 | ||||
-rw-r--r-- | test/regress/regress0/bug322.cvc | 23 | ||||
-rw-r--r-- | test/regress/regress0/bug322b.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/bug365.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/rec2.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress0/parallel-let.smt2 | 9 |
6 files changed, 60 insertions, 3 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 5eda230c3..58788c194 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -43,7 +43,8 @@ SMT2_TESTS = \ simple-lra.smt2 \ simple-rdl.smt2 \ simple-uf.smt2 \ - simplification_bug4.smt2 + simplification_bug4.smt2 \ + parallel-let.smt2 # Regression tests for PL inputs CVC_TESTS = \ @@ -115,7 +116,10 @@ BUG_TESTS = \ buggy-ite.smt2 \ bug303.smt2 \ bug310.cvc \ - bug339.smt2 + bug322.cvc \ + bug322b.cvc \ + bug339.smt2 \ + bug365.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug322.cvc b/test/regress/regress0/bug322.cvc new file mode 100644 index 000000000..c68fde795 --- /dev/null +++ b/test/regress/regress0/bug322.cvc @@ -0,0 +1,23 @@ +% EXPECT: sat +% EXIT: 10 +% Preamble -------------- +DATATYPE UNIT = Unit END; +DATATYPE BOOL = Truth | Falsity END; + +% Decls -------------- +node$type: TYPE; +value$type: TYPE; +Nodes$elem$type: TYPE = node$type; +Nodes$t$type: TYPE; +node_pair_set$type: TYPE = ARRAY node$type OF ARRAY node$type OF BOOL; +failure_pattern$type: TYPE = node_pair_set$type; +is_faulty:(node$type, failure_pattern$type) -> BOOL = (LAMBDA (p: node$type, + deliver: failure_pattern$type): + (IF (EXISTS (q: node$type): + (NOT ((((deliver)[ + (p)])[ + (q)]) = + (Truth)))) THEN + (Truth) ELSE (Falsity) ENDIF)); + +CHECKSAT; diff --git a/test/regress/regress0/bug322b.cvc b/test/regress/regress0/bug322b.cvc new file mode 100644 index 000000000..d10292dd5 --- /dev/null +++ b/test/regress/regress0/bug322b.cvc @@ -0,0 +1,12 @@ +% COMMAND-LINE: --incremental +% EXPECT: valid +% EXPECT: valid +% EXPECT: valid +% EXIT: 20 +x : INT; +y : INT = x + 1; +z : INT = -10; +identity : INT -> INT = LAMBDA(x:INT) : x; +QUERY identity(x) = x; +QUERY identity(y) > x; +QUERY identity(z) = -10; diff --git a/test/regress/regress0/bug365.smt2 b/test/regress/regress0/bug365.smt2 new file mode 100644 index 000000000..6dd48a849 --- /dev/null +++ b/test/regress/regress0/bug365.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_LIA) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(assert (let + ((a 2)) + (= a (let ((a 7)) a)))) +(check-sat) +(exit) + diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc index 80aecfe25..49684241c 100644 --- a/test/regress/regress0/datatypes/rec2.cvc +++ b/test/regress/regress0/datatypes/rec2.cvc @@ -1,7 +1,7 @@ % EXPECT: valid % EXIT: 20 c : BOOLEAN; -a16 : [# _a : REAL, _b : REAL #] = ( +a16 : [# _a : INT, _b : INT #] = ( IF c THEN (# _a := 3, _b := 2 #) ELSE (# _a := 1, _b := 5 #) ENDIF WITH ._a := 2); diff --git a/test/regress/regress0/parallel-let.smt2 b/test/regress/regress0/parallel-let.smt2 new file mode 100644 index 000000000..1f12522ee --- /dev/null +++ b/test/regress/regress0/parallel-let.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_UF) +(set-info :status unsat) +(declare-sort U 0) +(declare-fun x () U) +(declare-fun y () U) +(assert (distinct x y)) +(assert (let ((x y) (y x)) (= x y))) +(check-sat) +(exit) |