diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /test/regress/regress0/fmf | |
parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'test/regress/regress0/fmf')
-rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/fmf/bug651.smt2 | 43 | ||||
-rw-r--r-- | test/regress/regress0/fmf/bug652.smt2 | 22 |
3 files changed, 68 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index af8776ace..79cff2947 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -65,7 +65,9 @@ TESTS = \ memory_model-R_cpp-dd.cvc \ bug764.smt2 \ ko-bound-set.cvc \ - cons-sets-bounds.smt2 + cons-sets-bounds.smt2 \ + bug651.smt2 \ + bug652.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bug651.smt2 b/test/regress/regress0/fmf/bug651.smt2 new file mode 100644 index 000000000..9afc47972 --- /dev/null +++ b/test/regress/regress0/fmf/bug651.smt2 @@ -0,0 +1,43 @@ +; 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 () ( + (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) + + diff --git a/test/regress/regress0/fmf/bug652.smt2 b/test/regress/regress0/fmf/bug652.smt2 new file mode 100644 index 000000000..13748eeea --- /dev/null +++ b/test/regress/regress0/fmf/bug652.smt2 @@ -0,0 +1,22 @@ +; 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) |