diff options
Diffstat (limited to 'test/regress/regress0/fmf/dt-proper-model.smt2')
| -rw-r--r-- | test/regress/regress0/fmf/dt-proper-model.smt2 | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/test/regress/regress0/fmf/dt-proper-model.smt2 b/test/regress/regress0/fmf/dt-proper-model.smt2 deleted file mode 100644 index 0e66db996..000000000 --- a/test/regress/regress0/fmf/dt-proper-model.smt2 +++ /dev/null @@ -1,16 +0,0 @@ -; COMMAND-LINE: --finite-model-find -; EXPECT: sat -(set-logic ALL_SUPPORTED) -(set-info :status sat) -(declare-sort U 0) -(declare-datatypes ((D 0)) (((cons (x Int) (y U))))) -(declare-fun d1 () D) -(declare-fun d2 () D) -(declare-fun d3 () D) -(declare-fun d4 () D) -(assert (distinct d1 d2 d3 d4)) -(assert (forall ((x U) (y U)) (= x y))) -(declare-fun a () U) -(declare-fun P (U) Bool) -(assert (P a)) -(check-sat) |