diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 13:43:31 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 13:43:37 -0600 |
| commit | d2e45128356c725d479a3efff475d8e5f430e4f3 (patch) | |
| tree | f28916d982f359bad1147a22b3d3526f02f538d0 /test | |
| parent | 1ce3fb16b0e0e3a51713d643e792499775a7f11b (diff) | |
Fix boolean term conversion for INST_ATTRIBUTE, fixes bug 764.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/bug764.smt2 | 28 |
2 files changed, 30 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index d734a6b95..218dde7d4 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -62,7 +62,8 @@ TESTS = \ fmf-strange-bounds.smt2 \ fmf-strange-bounds-2.smt2 \ fmf-bound-2dim.smt2 \ - memory_model-R_cpp-dd.cvc + memory_model-R_cpp-dd.cvc \ + bug764.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bug764.smt2 b/test/regress/regress0/fmf/bug764.smt2 new file mode 100644 index 000000000..d030c3e88 --- /dev/null +++ b/test/regress/regress0/fmf/bug764.smt2 @@ -0,0 +1,28 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(define-fun BoolToString ((b Bool)) String (ite b "true" "false") ) + +(declare-datatypes () ( + (Color (red) (white) (blue)) +) ) + +(define-fun ColorToString ((c Color)) String (ite (is-red c) "red" (ite (is-white c) "white" "blue")) ) + +(declare-datatypes () ( + (CP (cp (b Bool) (c Color))) +) ) + +(define-fun-rec CPToString ((cp CP)) String (str.++ "cp(" (BoolToString (b cp)) "," (ColorToString (c cp)) ")")) + +(declare-fun CPFromString (String) CP) + +(assert (forall ((cp1 CP)) (= cp1 (CPFromString (CPToString cp1))))) + +(declare-fun cpx() CP) +(assert (= cpx (CPFromString "cp(true,white)"))) + +(check-sat) + |