diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress1/crash_burn_locusts.smt2 | |
parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress1/crash_burn_locusts.smt2')
-rw-r--r-- | test/regress/regress1/crash_burn_locusts.smt2 | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/test/regress/regress1/crash_burn_locusts.smt2 b/test/regress/regress1/crash_burn_locusts.smt2 new file mode 100644 index 000000000..313d6f79c --- /dev/null +++ b/test/regress/regress1/crash_burn_locusts.smt2 @@ -0,0 +1,29 @@ +;; 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) +)) |