7 files changed, 76 insertions, 5 deletions
diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
index 536bc241f..f62f057e4 100644
--- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
+++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --finite-model-find
+% COMMAND-LINE: --finite-model-find --mbqi=gen-ev
 % EXPECT: unsat
 (benchmark Isabelle
 :status sat
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index b9a87231f..395054d67 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -23,18 +23,23 @@ TESTS =	\
 	agree466.smt2 \
 	ALG008-1.smt2 \
 	german169.smt2 \
-	Hoare-z3.931718.smt \
 	QEpres-uf.855035.smt \
 	agree467.smt2 \
 	Arrow_Order-smtlib.778341.smt \
 	german73.smt2 \
 	PUZ001+1.smt2 \
 	refcount24.cvc.smt2 \
-	bug0909.smt2 \
-	fmf-bound-int.smt2
+	fmf-bound-int.smt2 \
+	fc-simple.smt2 \
+	fc-unsat-tot-2.smt2 \
+	fc-unsat-pent.smt2 \
+	fc-pigeonhole19.smt2
 
 EXTRA_DIST = $(TESTS)
 
+# disabled for now :
+# Hoare-z3.931718.smt bug0909.smt2
+
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
 #TESTS += \
diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt
index 980e5fd49..2945c8f4d 100644
--- a/test/regress/regress0/fmf/QEpres-uf.855035.smt
+++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --finite-model-find
+% COMMAND-LINE: --finite-model-find --mbqi=gen-ev
 % EXPECT: sat
 (benchmark Isabelle
 :status sat
diff --git a/test/regress/regress0/fmf/fc-pigeonhole19.smt2 b/test/regress/regress0/fmf/fc-pigeonhole19.smt2
new file mode 100755
index 000000000..15c36682c
--- /dev/null
+++ b/test/regress/regress0/fmf/fc-pigeonhole19.smt2
@@ -0,0 +1,20 @@
+(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort P 0)
+(declare-sort H 0)
+
+(declare-fun p () P)
+(declare-fun h () H)
+
+; pigeonhole using native cardinality constraints
+(assert (fmf.card p 19))
+(assert (not (fmf.card p 18)))
+(assert (fmf.card h 18))
+(assert (not (fmf.card h 17)))
+
+; each pigeon has different holes
+(declare-fun f (P) H)
+(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))
+
+(check-sat)
+\ No newline at end of file
diff --git a/test/regress/regress0/fmf/fc-simple.smt2 b/test/regress/regress0/fmf/fc-simple.smt2
new file mode 100755
index 000000000..d1fd2301c
--- /dev/null
+++ b/test/regress/regress0/fmf/fc-simple.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun c () U)
+
+(assert (fmf.card c 2))
+(assert (not (fmf.card a 4)))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2
new file mode 100755
index 000000000..f1721cb04
--- /dev/null
+++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2
@@ -0,0 +1,20 @@
+(set-logic QF_UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+
+(assert (not (= a b)))
+(assert (not (= b c)))
+(assert (not (= c d)))
+(assert (not (= d e)))
+(assert (not (= e a)))
+
+(assert (fmf.card c 2))
+
+(check-sat)
+\ No newline at end of file
diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
new file mode 100755
index 000000000..d946974ed
--- /dev/null
+++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
@@ -0,0 +1,14 @@
+(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+
+(assert (not (fmf.card a 2)))
+
+(assert (forall ((x U)) (or (= x a) (= x b))))
+
+(check-sat)
+\ No newline at end of file