From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 25 May 2015 08:35:00 +0000 (+0200)
Subject: Add missing regression
X-Git-Tag: cvc5-1.0.0~6323
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd5b8c7aa15b9a2d84836e712c8dc61667afb348;p=cvc5.git

Add missing regression
---

diff --git a/test/regress/regress0/uf/cnf-and-neg.smt2 b/test/regress/regress0/uf/cnf-and-neg.smt2
new file mode 100755
index 000000000..711740f67
--- /dev/null
+++ b/test/regress/regress0/uf/cnf-and-neg.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort I 0)
+(declare-fun a () I)
+(declare-fun b () I)
+(declare-fun c () I)
+(declare-fun f (I) I)
+(assert (not (= (f a) (f b))))
+(assert (not (= (f a) (f c))))
+(assert (not (and (not (= a b)) (not (= a c)))))
+(check-sat)