From cd5b8c7aa15b9a2d84836e712c8dc61667afb348 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 25 May 2015 10:35:00 +0200 Subject: [PATCH] Add missing regression --- test/regress/regress0/uf/cnf-and-neg.smt2 | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100755 test/regress/regress0/uf/cnf-and-neg.smt2 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) -- 2.30.2