summaryrefslogtreecommitdiff
path: root/test/regress/regress0/crash_burn_locusts.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/crash_burn_locusts.smt2')
-rw-r--r--test/regress/regress0/crash_burn_locusts.smt229
1 files changed, 0 insertions, 29 deletions
diff --git a/test/regress/regress0/crash_burn_locusts.smt2 b/test/regress/regress0/crash_burn_locusts.smt2
deleted file mode 100644
index 313d6f79c..000000000
--- a/test/regress/regress0/crash_burn_locusts.smt2
+++ /dev/null
@@ -1,29 +0,0 @@
-;; This is a nasty parsing test for define-fun-rec
-
-(set-logic UFLIRA)
-(set-info :smt-lib-version 2.5)
-(define-fun-rec (
- (f ((x Int)) Int 5) ;; ok, f : Int -> Int
- (g ((x Int)) Int (h 4)) ;; um, ok, so g : Int -> Int and h : Int -> Int?
- (h ((x Real)) Int 4) ;; oops no we were wrong, **CRASH**
-))
-
-(reset)
-
-(set-logic UFLIRA)
-(set-info :smt-lib-version 2.5)
-(define-fun-rec (
- (f ((x Int)) Int (g (h 4) 5)) ;; ok, f : Int -> Int and g : Int -> X -> Int and h : Int -> X ??! What the F?! (pun intended)
- (g ((x Int)) Int 5) ;; wait, now g has wrong arity?!! **BURN**
- (h ((x Int)) Int 2)
-))
-
-(reset)
-
-(set-logic UFLIRA)
-(set-info :smt-lib-version 2.5)
-(declare-const g Int 2)
-(define-fun-rec (
- (f () Int g) ;; wait, which g does this refer to?! **LOCUSTS**
- (g () Int 5)
-))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback