From 781bfd65daec2932b7836259b3484ac500edb46a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Apr 2018 19:59:59 -0500
Subject: Fix alpha equivalence for higher-order (#1769)

---
 test/regress/Makefile.tests                    |  1 +
 test/regress/regress0/ho/fta0144-alpha-eq.smt2 | 29 ++++++++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 test/regress/regress0/ho/fta0144-alpha-eq.smt2

(limited to 'test')

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 3899ff367..76185044e 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -444,6 +444,7 @@ REG0_TESTS = \
 	regress0/ho/ext-sat-partial-eval.smt2 \
 	regress0/ho/ext-sat.smt2 \
 	regress0/ho/finite-fun-ext.smt2 \
+	regress0/ho/fta0144-alpha-eq.smt2 \
 	regress0/ho/ho-match-fun-suffix.smt2 \
 	regress0/ho/ho-matching-enum.smt2 \
 	regress0/ho/ho-matching-nested-app.smt2 \
diff --git a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 b/test/regress/regress0/ho/fta0144-alpha-eq.smt2
new file mode 100644
index 000000000..0fc536bd9
--- /dev/null
+++ b/test/regress/regress0/ho/fta0144-alpha-eq.smt2
@@ -0,0 +1,29 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort Nat$ 0)
+(declare-sort Complex$ 0)
+(declare-sort Real_set$ 0)
+(declare-fun g$ (Nat$) Complex$)
+(declare-fun r$ () Real)
+(declare-fun uu$ (Real Real) Real)
+(declare-fun uua$ (Real_set$ Real) Bool)
+(declare-fun less$ (Nat$ Nat$) Bool)
+(declare-fun norm$ (Complex$) Real)
+(declare-fun zero$ () Complex$)
+(declare-fun minus$ (Complex$ Complex$) Complex$)
+(declare-fun norm$a (Real) Real)
+(declare-fun zero$a () Nat$)
+(declare-fun member$ (Real Real_set$) Bool)
+(declare-fun minus$a (Nat$ Nat$) Nat$)
+(declare-fun thesis$ () Bool)
+(declare-fun collect$ ((-> Real Bool)) Real_set$)
+(declare-fun less_eq$ (Nat$ Nat$) Bool)
+(declare-fun strict_mono$ ((-> Nat$ Nat$)) Bool)
+(declare-fun strict_mono$a ((-> Real Real)) Bool)
+(declare-fun strict_mono$b ((-> Nat$ Real)) Bool)
+(declare-fun strict_mono$c ((-> Real Nat$)) Bool)
+(assert (! (not thesis$) :named a2))
+(assert (! (forall ((?v0 (-> Nat$ Nat$)) (?v1 Complex$)) (=> (and true (forall ((?v2 Real)) (=> true (exists ((?v3 Nat$)) (forall ((?v4 Nat$)) (=> (less_eq$ ?v3 ?v4) (< (norm$ (minus$ (g$ (?v0 ?v4)) ?v1)) ?v2))))))) thesis$)) :named a3))
+(assert (! (exists ((?v0 (-> Nat$ Nat$)) (?v1 Complex$)) (and true (forall ((?v2 Real)) (=> true (exists ((?v3 Nat$)) (forall ((?v4 Nat$)) (=> (less_eq$ ?v3 ?v4) (< (norm$ (minus$ (g$ (?v0 ?v4)) ?v1)) ?v2)))))))) :named a4))
+(check-sat)
-- 
cgit v1.2.3