diff options
Diffstat (limited to 'test/regress/regress0/ho/fta0144-alpha-eq.smt2')
| -rw-r--r-- | test/regress/regress0/ho/fta0144-alpha-eq.smt2 | 29 |
1 files changed, 29 insertions, 0 deletions
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) |