diff options
Diffstat (limited to 'test/regress/regress0/fmf/bug652.smt2')
| -rw-r--r-- | test/regress/regress0/fmf/bug652.smt2 | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/test/regress/regress0/fmf/bug652.smt2 b/test/regress/regress0/fmf/bug652.smt2 deleted file mode 100644 index 13748eeea..000000000 --- a/test/regress/regress0/fmf/bug652.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -; COMMAND-LINE: --fmf-fun --no-check-models -; EXPECT: sat -(set-logic UFDTSLIA) -(set-info :smt-lib-version 2.5) -(set-option :produce-models true) - -(declare-datatypes () ( - (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean))) -) ) - -(define-funs-rec - ( - (f4208$lengthList_boolean((x List_boolean)) Int) - ) - ( - (ite (is-List_boolean$CNil_boolean x) 0 (+ 1 (f4208$lengthList_boolean (List_boolean$Cstr_boolean$tail x)))) - ) -) - - -(declare-const boolean Bool) -(check-sat) |