From 081351e87edeb52facba0d0abc2e933433480444 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 15 Jan 2016 00:18:49 +0100
Subject: Ensure model construction for parametric sorts involving
 uninterpreted sorts respect cardinality bounds on when finite model finding
 is enabled.

---
 test/regress/regress0/fmf/Makefile.am          |  8 +++++---
 test/regress/regress0/fmf/dt-proper-model.smt2 | 16 ++++++++++++++++
 2 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100755 test/regress/regress0/fmf/dt-proper-model.smt2

(limited to 'test/regress/regress0/fmf')

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index bca9f2e4f..5abadbcb8 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -20,7 +20,6 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 TESTS =	\
 	array_card.smt2 \
-	agree466.smt2 \
 	ALG008-1.smt2 \
 	german169.smt2 \
 	QEpres-uf.855035.smt \
@@ -43,7 +42,8 @@ TESTS =	\
 	syn002-si-real-int.smt2 \
 	krs-sat.smt2 \
 	forall_unit_data2.smt2 \
-	sc_bad_model_1221.smt2
+  sc_bad_model_1221.smt2 \
+  dt-proper-model.smt2
 
 
 EXTRA_DIST = $(TESTS)
@@ -54,11 +54,13 @@ EXTRA_DIST = $(TESTS)
 #TESTS += \
 #	error.cvc
 #endif
-#
+# 
 # and make sure to distribute it
 #EXTRA_DIST += \
 #	error.cvc
 
+# agree466.smt2 timeout after commit on 1/14 due to Array+FMF model construction
+
 # synonyms for "check" in this directory
 .PHONY: regress regress0 test
 regress regress0 test: check
diff --git a/test/regress/regress0/fmf/dt-proper-model.smt2 b/test/regress/regress0/fmf/dt-proper-model.smt2
new file mode 100755
index 000000000..60a0b6377
--- /dev/null
+++ b/test/regress/regress0/fmf/dt-proper-model.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-sort U 0)
+(declare-datatypes () ((D (cons (x Int) (y U)))))
+(declare-fun d1 () D)
+(declare-fun d2 () D)
+(declare-fun d3 () D)
+(declare-fun d4 () D)
+(assert (distinct d1 d2 d3 d4))
+(assert (forall ((x U) (y U)) (= x y)))
+(declare-fun a () U)
+(declare-fun P (U) Bool)
+(assert (P a))
+(check-sat)
\ No newline at end of file
-- 
cgit v1.2.3