From 612509379a1417f8d4a5e001ff143ba819f5516f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 23 Nov 2017 20:07:19 -0600 Subject: Ho parsing and regressions (#1350) --- test/regress/regress0/ho/ho-matching-enum-2.smt2 | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 test/regress/regress0/ho/ho-matching-enum-2.smt2 (limited to 'test/regress/regress0/ho/ho-matching-enum-2.smt2') diff --git a/test/regress/regress0/ho/ho-matching-enum-2.smt2 b/test/regress/regress0/ho/ho-matching-enum-2.smt2 new file mode 100644 index 000000000..9581e4c4f --- /dev/null +++ b/test/regress/regress0/ho/ho-matching-enum-2.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun p (Int) Bool) +(declare-fun q (Int) Bool) +(declare-fun k (Int Int) Int) + +(assert (q (k 0 1))) +(assert (not (p (k 0 0)))) + +(assert (forall ((f (-> Int Int Int)) (y Int) (z Int)) (or (p (f y z)) (not (q (f z y)))))) + +(check-sat) +(exit) -- cgit v1.2.3