diff options
Diffstat (limited to 'test/regress/regress1/fmf/constr-ground-to.smt2')
| -rw-r--r-- | test/regress/regress1/fmf/constr-ground-to.smt2 | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/test/regress/regress1/fmf/constr-ground-to.smt2 b/test/regress/regress1/fmf/constr-ground-to.smt2 new file mode 100644 index 000000000..bc6d9e948 --- /dev/null +++ b/test/regress/regress1/fmf/constr-ground-to.smt2 @@ -0,0 +1,43 @@ +; COMMAND-LINE: --fmf-fun --lang=smt2.5 +; 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) |