diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-19 18:15:21 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-09 18:27:41 -0400 |
| commit | 28ec8ce392a815c47689ecd86b5b91f9a58104e5 (patch) | |
| tree | a48183cf1ce4f28653f994e15b7191c3f4005165 /test/unit/parser | |
| parent | e5044d89c715ac6c0d41a731b58a9c672d2d524e (diff) | |
Add support for check-sat with argument.
Diffstat (limited to 'test/unit/parser')
| -rw-r--r-- | test/unit/parser/parser_black.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 1dbaf7cdf..8ff62c25a 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -395,7 +395,7 @@ public: #ifndef CVC4_COMPETITION_MODE tryBadInput("(assert)"); // no args tryBadInput("(set-info :notes |Symbols can't contain the | character|)"); - tryBadInput("(set-logic QF_UF) (check-sat true)"); // shouldn't have an arg + tryBadInput("(set-logic QF_UF) (check-sat true)", true); // check-sat shouldn't have an arg tryBadInput("(declare-sort a)"); // no arg tryBadInput("(declare-sort a 0) (declare-sort a 0)"); // double decl tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); // should be "p () Bool" |