Correct subtyping for arrays, disable subtyping for predicate subtypes. Bug fixes in quantifiers related to subtypes/parametric sorts. Make macros trace dependencies for get-unsat-core. Add regressions.

5 files changed, 69 insertions, 1 deletions

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index df146752e..02eaeeb47 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -70,7 +70,11 @@ TESTS =	\
   agg-rew-test.smt2 \
   agg-rew-test-cf.smt2 \
   rew-to-0211-dd.smt2 \
-  rew-to-scala.smt2
+  rew-to-scala.smt2 \
+  macro-subtype-param.smt2 \
+  macros-real-arg.smt2 \
+  subtype-param-unk.smt2 \
+  subtype-param.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
new file mode 100644
index 000000000..20de79047
--- /dev/null
+++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: unknown
+; this will fail if type rule for APPLY_UF requires to be subtypes
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+(assert (forall ((x (List Int))) (R x)))
+(declare-fun j1 () (List Real))
+(assert (not (R j1)))
+
+(declare-fun Q ((Array Real Int)) Bool)
+(assert (forall ((x (Array Real Int))) (Q x)))
+(declare-fun j2 () (Array Int Real))
+(assert (not (Q j2)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2
new file mode 100644
index 000000000..675c96d68
--- /dev/null
+++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: unsat
+; this will fail if type rule for APPLY_UF is made strict
+(set-logic UFLIRA)
+(declare-fun P (Int) Bool)
+(assert (forall ((x Int)) (P x)))
+(declare-fun k () Real)
+(declare-fun k2 () Int)
+(assert (or (not (P k)) (not (P k2))))
+(assert (= k 0))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2
new file mode 100644
index 000000000..836449cb9
--- /dev/null
+++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: 
+; EXPECT: unknown
+; this will fail if type rule for APPLY_UF requires arguments to be subtypes
+(set-logic ALL_SUPPORTED)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+
+(assert (forall ((x (List Int))) (R x)))
+(declare-fun j1 () (List Real))
+(assert (not (R j1)))
+
+(declare-fun Q ((Array Int Real)) Bool)
+(assert (forall ((x (Array Int Int))) (Q x)))
+(declare-fun j2 () (Array Int Real))
+(assert (not (Q j2)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2
new file mode 100644
index 000000000..08615abf6
--- /dev/null
+++ b/test/regress/regress0/quantifiers/subtype-param.smt2
@@ -0,0 +1,16 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil))))
+
+(declare-fun R ((List Int)) Bool)
+(assert (forall ((x (List Real))) (R x)))
+
+(declare-fun Q ((Array Int Real)) Bool)
+(assert (forall ((x (Array Int Int))) (Q x)))
+
+(declare-fun k1 () (List Int))
+(declare-fun k2 () (Array Real Int))
+(assert (or (not (R k1)) (not (Q k2))))
+
+(check-sat)