diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-01 22:44:40 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-01 22:44:40 +0200 |
| commit | cbcc5124a8f0f17acd981a80c182616cd0a778ff (patch) | |
| tree | 0a77487acde8a9a05762b7dcfe436c76defb1f0b /test/regress/regress0/uf | |
| parent | 7f85896a9f1c9d3c8f65c53c16fea2156bc4dfab (diff) | |
When proof enabled, disable uf sym break. Add regression.
Diffstat (limited to 'test/regress/regress0/uf')
| -rw-r--r-- | test/regress/regress0/uf/Makefile.am | 3 | ||||
| -rwxr-xr-x | test/regress/regress0/uf/cnf_abc.smt2 | 168 |
2 files changed, 170 insertions, 1 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 50de00b61..c9a47c26f 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -49,7 +49,8 @@ TESTS = \ cnf-iff.smt2 \ cnf-iff-base.smt2 \ cnf-ite.smt2 \ - cnf-and-neg.smt2 + cnf-and-neg.smt2 \ + cnf_abc.smt2 EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/cnf_abc.smt2 b/test/regress/regress0/uf/cnf_abc.smt2 new file mode 100755 index 000000000..5d011f44c --- /dev/null +++ b/test/regress/regress0/uf/cnf_abc.smt2 @@ -0,0 +1,168 @@ +(set-logic QF_UF)
+(set-info :status unsat)
+
+(declare-sort I 0)
+(declare-fun f (I I) I)
+(declare-fun a () I)
+(declare-fun b () I)
+(declare-fun c () I)
+
+
+
+(assert
+ (or
+ (= (f a a) a)
+ (= (f a a) b)
+ (= (f a a) c)
+ ))
+
+(assert
+ (or
+ (= (f a b) a)
+ (= (f a b) b)
+ (= (f a b) c)
+ ))
+
+(assert
+ (or
+ (= (f a c) a)
+ (= (f a c) b)
+ (= (f a c) c)
+ ))
+
+(assert
+ (or
+ (= (f b a) a)
+ (= (f b a) b)
+ (= (f b a) c)
+ ))
+
+(assert
+ (or
+ (= (f b b) a)
+ (= (f b b) b)
+ (= (f b b) c)
+ ))
+
+(assert
+ (or
+ (= (f b c) a)
+ (= (f b c) b)
+ (= (f b c) c)
+ ))
+
+
+(assert
+ (or
+ (= (f c a) a)
+ (= (f c a) b)
+ (= (f c a) c)
+ ))
+
+(assert
+ (or
+ (= (f c b) a)
+ (= (f c b) b)
+ (= (f c b) c)
+ ))
+
+(assert
+ (or
+ (= (f c c) a)
+ (= (f c c) b)
+ (= (f c c) c)
+ ))
+
+
+
+(assert
+ (or
+ (= (f a a) a)
+ (= (f b b) a)
+ (= (f c c) a)
+ ))
+
+(assert
+ (or
+ (= (f a a) b)
+ (= (f b b) b)
+ (= (f c c) b)
+ ))
+
+(assert
+ (or
+ (= (f a a) c)
+ (= (f b b) c)
+ (= (f c c) c)
+ ))
+
+
+
+(assert
+ (or
+ (= (f a a) a)
+ (= (f b a) b)
+ (= (f c a) c)
+ ))
+
+(assert
+ (or
+ (= (f a b) a)
+ (= (f b b) b)
+ (= (f c b) c)
+ ))
+
+(assert
+ (or
+ (= (f a c) a)
+ (= (f b c) b)
+ (= (f c c) c)
+ ))
+
+
+
+
+(assert (not (= (f a a) a)))
+(assert (not (= (f b b) b)))
+(assert (not (= (f c c) c)))
+
+
+(assert
+ (or
+ (not (= (f a (f a a)) a))
+ (not (= (f a (f a b)) b))
+ (not (= (f a (f a c)) c))
+ ))
+
+(assert
+ (or
+ (not (= (f b (f b a)) a))
+ (not (= (f b (f b b)) b))
+ (not (= (f b (f b c)) c))
+ ))
+
+(assert
+ (or
+ (not (= (f c (f c a)) a))
+ (not (= (f c (f c b)) b))
+ (not (= (f c (f c c)) c))
+ ))
+
+
+(assert (not (= (f a a) (f b a))))
+(assert (not (= (f a a) (f c a))))
+(assert (not (= (f b a) (f c a))))
+
+(assert (not (= (f a b) (f b b))))
+(assert (not (= (f a b) (f c b))))
+(assert (not (= (f b b) (f c b))))
+
+(assert (not (= (f a c) (f b c))))
+(assert (not (= (f a c) (f c c))))
+(assert (not (= (f b c) (f c c))))
+
+
+
+(check-sat)
+
+(exit)
|