diff options
| author | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 10:45:04 -0700 |
|---|---|---|
| committer | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 10:45:04 -0700 |
| commit | 9f2ff7173d434162d49814ba3f24a9f9db21d476 (patch) | |
| tree | f56f01b17d1233b2820fea26d259984c0b6d1c83 /test/regress/regress0/fmf | |
| parent | d4afd65c3dcc26bab066507356ad187cbcb23d9e (diff) | |
| parent | 0daf670d46ec2e781c2060b41449f2787b6e8f66 (diff) | |
Merge branch 'master' into google
Diffstat (limited to 'test/regress/regress0/fmf')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile | 8 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/PUZ001+1.smt2 | 2 |
2 files changed, 9 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile b/test/regress/regress0/fmf/Makefile new file mode 100644 index 000000000..1e68a1e9e --- /dev/null +++ b/test/regress/regress0/fmf/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/fmf + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/fmf/PUZ001+1.smt2 b/test/regress/regress0/fmf/PUZ001+1.smt2 index f0e53fc98..f3db78491 100644 --- a/test/regress/regress0/fmf/PUZ001+1.smt2 +++ b/test/regress/regress0/fmf/PUZ001+1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --no-check-proofs +; COMMAND-LINE: --finite-model-find --no-check-proofs --no-check-unsat-core ; EXPECT: unsat ;%------------------------------------------------------------------------------ ;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. |