diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-05 09:56:00 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-05 09:56:00 -0500 |
| commit | abb71e0d55b23fcd28872866b64ffe64f76d1ee6 (patch) | |
| tree | 5a4da709b0dadc931ff73bdf6bb389f6c01967ee /test | |
| parent | c77213eaf165746a3704204ce56915b86c5f2a7a (diff) | |
Caching for fun def process, add regression.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/constr-ground-to.smt2 | 43 |
2 files changed, 45 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index be2a274b2..730108ee7 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -69,7 +69,8 @@ TESTS = \ bug651.smt2 \ bug652.smt2 \ bug782.smt2 \ - quant_real_univ.cvc + quant_real_univ.cvc \ + constr-ground-to.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/constr-ground-to.smt2 b/test/regress/regress0/fmf/constr-ground-to.smt2 new file mode 100644 index 000000000..c8f6c1d71 --- /dev/null +++ b/test/regress/regress0/fmf/constr-ground-to.smt2 @@ -0,0 +1,43 @@ +; COMMAND-LINE: --fmf-fun +; EXPECT: sat +(set-logic UFDTLIA) +(declare-datatypes () ( + ( + Term + (str (sv IntList)) + ) + ( + IntList + (sn) + (sc (sh Int) (st IntList)) + ) +)) +(declare-const t Term) +(assert ( + and + (is-str t) + (is-sc (sv t)) + (is-sc (st (sv t))) + (is-sc (st (st (sv t)))) + (is-sc (st (st (st (sv t))))) + (is-sc (st (st (st (st (sv t)))))) + (is-sc (st (st (st (st (st (sv t))))))) + (is-sc (st (st (st (st (st (st (sv t)))))))) + (is-sc (st (st (st (st (st (st (st (sv t))))))))) + (is-sc (st (st (st (st (st (st (st (st (sv t)))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (sv t))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t))))))))))))))))))))))) + (is-sc (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (st (sv t)))))))))))))))))))))))) +)) +(check-sat) |