diff options
Diffstat (limited to 'test/regress/regress0/fmf')
-rw-r--r-- | test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt | 2 | ||||
-rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 12 | ||||
-rw-r--r-- | test/regress/regress0/fmf/QEpres-uf.855035.smt | 2 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/fc-pigeonhole19.smt2 | 20 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/fc-simple.smt2 | 12 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/fc-unsat-pent.smt2 | 20 | ||||
-rwxr-xr-x | test/regress/regress0/fmf/fc-unsat-tot-2.smt2 | 14 |
7 files changed, 77 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..e3bfd39b8 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -23,18 +23,24 @@ 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 \ + Hoare-z3.931718.smt EXTRA_DIST = $(TESTS) +# disabled for now : +# 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 |