diff options
Diffstat (limited to 'test/regress/regress1/fmf/bug651.smt2')
-rw-r--r-- | test/regress/regress1/fmf/bug651.smt2 | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/test/regress/regress1/fmf/bug651.smt2 b/test/regress/regress1/fmf/bug651.smt2 new file mode 100644 index 000000000..bcfeebd69 --- /dev/null +++ b/test/regress/regress1/fmf/bug651.smt2 @@ -0,0 +1,43 @@ +; COMMAND-LINE: --fmf-fun --no-check-models --lang=smt2.5 +; EXPECT: sat +(set-logic UFDTSLIA) +(set-info :smt-lib-version 2.5) +(set-option :produce-models true) + +(declare-datatypes () ( + (Conditional_Int (Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int))) + (Conditional_T_titleType (Conditional_T_titleType$CAbsent_T_titleType) (Conditional_T_titleType$CPresent_T_titleType (Conditional_T_titleType$CPresent_T_titleType$value T_titleType))) + (Conditional_boolean (Conditional_boolean$CAbsent_boolean) (Conditional_boolean$CPresent_boolean (Conditional_boolean$CPresent_boolean$value Bool))) + (Conditional_string (Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String))) + (Double (Double$CINF) (Double$CNINF) (Double$CNaN) (Double$CValue (Double$CValue$value Int))) + (List_T_titleType (List_T_titleType$CNil_T_titleType) (List_T_titleType$Cstr_T_titleType (List_T_titleType$Cstr_T_titleType$head T_titleType) (List_T_titleType$Cstr_T_titleType$tail List_T_titleType))) + (List_boolean (List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean))) + (List_string (List_string$CNil_string) (List_string$Cstr_string (List_string$Cstr_string$head String) (List_string$Cstr_string$tail List_string))) + (T_titleType (T_titleType$C_T_titleType (T_titleType$C_T_titleType$base String))) +) ) + +(define-fun f1361$isValid_string((x String)) Bool true) +(define-fun f5131$isValid_T_titleType((x T_titleType)) Bool (and (f1361$isValid_string (T_titleType$C_T_titleType$base x)) (<= (str.len (T_titleType$C_T_titleType$base x)) 80))) +(define-funs-rec + ( + (f5242$isValidElementsList_T_titleType((x List_T_titleType)) Bool) + ) + ( + (=> (is-List_T_titleType$Cstr_T_titleType x) (and (f5131$isValid_T_titleType (List_T_titleType$Cstr_T_titleType$head x)) (f5242$isValidElementsList_T_titleType (List_T_titleType$Cstr_T_titleType$tail x)))) + ) +) +(define-fun f1348$isValid_boolean((x Bool)) Bool true) +(define-funs-rec + ( + (f4169$isValidElementsList_boolean((x List_boolean)) Bool) + ) + ( + (=> (is-List_boolean$Cstr_boolean x) (and (f1348$isValid_boolean (List_boolean$Cstr_boolean$head x)) (f4169$isValidElementsList_boolean (List_boolean$Cstr_boolean$tail x)))) + ) +) + + +(declare-const title T_titleType) +(check-sat) + + |