diff options
Diffstat (limited to 'test/regress')
8 files changed, 35 insertions, 8 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 17a2ea2ef..1368dd067 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -189,6 +189,7 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) # we have a minimized version still getting tested # bug639 -- still fails, reopened bug # bug585 -- contains subrange type (not supported) +# issue1048-arrays-int-real.smt2 -- different errors on debug and production DISABLED_TESTS = \ bug512.smt2 \ bug585.cvc diff --git a/test/regress/regress0/datatypes/tuple-no-clash.cvc b/test/regress/regress0/datatypes/tuple-no-clash.cvc index 4d7345a54..ecdc8198f 100644 --- a/test/regress/regress0/datatypes/tuple-no-clash.cvc +++ b/test/regress/regress0/datatypes/tuple-no-clash.cvc @@ -6,6 +6,6 @@ y : REAL; z : REAL; ASSERT x = (y, z) OR x = (z, y); -ASSERT x = (0,0) OR x = (1,1); +ASSERT x = (0.0,0.0) OR x = (1.0,1.0); CHECKSAT; diff --git a/test/regress/regress0/issue1048-arrays-int-real.smt2 b/test/regress/regress0/issue1048-arrays-int-real.smt2 new file mode 100644 index 000000000..6bbfe4cb7 --- /dev/null +++ b/test/regress/regress0/issue1048-arrays-int-real.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_ALIRA) +(declare-fun a () (Array Int Real)) +(declare-fun b () (Array Int Int)) +(assert (= a b)) +(assert (= (select a 0) 0.5)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index c5a81c960..cdf2ec9bc 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -70,10 +70,7 @@ TESTS = \ agg-rew-test-cf.smt2 \ rew-to-0211-dd.smt2 \ rew-to-scala.smt2 \ - macro-subtype-param.smt2 \ macros-real-arg.smt2 \ - subtype-param-unk.smt2 \ - subtype-param.smt2 \ anti-sk-simp.smt2 \ pure_dt_cbqi.smt2 \ florian-case-ax.smt2 \ @@ -108,6 +105,11 @@ TESTS = \ # clock-10.smt2 # +# FIXME: I've disabled these since they give different error messages on production and debug +# macro-subtype-param.smt2 +# subtype-param-unk.smt2 +# subtype-param.smt2 + EXTRA_DIST = $(TESTS) \ bug291.smt2.expect diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 index f44d75195..97ff827a7 100644 --- a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 @@ -1,5 +1,11 @@ ; COMMAND-LINE: --macros-quant -; EXPECT: unknown +; EXPECT: (error "argument type is not a subtype of the function's argument type: +; EXPECT: argument: x +; EXPECT: has type: (List Int) +; EXPECT: not subtype: (List Real) +; EXPECT: in term : (R (as x (List Real)))") +; EXIT: 1 + (set-logic ALL_SUPPORTED) (declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil))))) diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 index e3008772d..f3ee6a86a 100644 --- a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 @@ -1,5 +1,11 @@ ; COMMAND-LINE: --lang=smt2.5 -; EXPECT: unknown +; EXPECT: (error "argument type is not a subtype of the function's argument type: +; EXPECT: argument: x +; EXPECT: has type: (List Int) +; EXPECT: not subtype: (List Real) +; EXPECT: in term : (R (as x (List Real)))") +; EXIT: 1 + ; this will fail if type rule for APPLY_UF requires arguments to be subtypes (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2 index 42d7a5b60..860c03b6f 100644 --- a/test/regress/regress0/quantifiers/subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param.smt2 @@ -1,5 +1,11 @@ ; COMMAND-LINE: --lang=smt2.5 -; EXPECT: unsat +; EXPECT: (error "argument type is not a subtype of the function's argument type: +; EXPECT: argument: x +; EXPECT: has type: (Array Int Int) +; EXPECT: not subtype: (Array Int Real) +; EXPECT: in term : (Q (as x (Array Int Real)))") +; EXIT: 1 + (set-logic ALL_SUPPORTED) (set-info :status unsat) diff --git a/test/regress/regress0/sets/sets-tuple-poly.cvc b/test/regress/regress0/sets/sets-tuple-poly.cvc index 64fb310be..4cac9a24e 100644 --- a/test/regress/regress0/sets/sets-tuple-poly.cvc +++ b/test/regress/regress0/sets/sets-tuple-poly.cvc @@ -7,7 +7,7 @@ b : SET OF [INT, REAL]; x : [ REAL, REAL ]; -ASSERT NOT x = (0,0); +ASSERT NOT x = (0.0,0.0); ASSERT (x.0, FLOOR(x.1)) IS_IN a; ASSERT (FLOOR(x.0), x.1) IS_IN b; |