diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-22 02:51:31 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-22 02:53:25 -0400 |
| commit | 19f565aabe8ece904f67e1353ec67a5bf485fc97 (patch) | |
| tree | e6a4c6af9906fc2d4f26b0c5b9d10d88a0827faa | |
| parent | 06a53c4dbe1cafe56fc4e1b7e2f6f8cd7b5a66b3 (diff) | |
Final fixes for smtcomp2014-application.
| -rwxr-xr-x | contrib/run-script-smtcomp2014-application | 3 | ||||
| -rw-r--r-- | src/main/driver_unified.cpp | 1 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 |
3 files changed, 7 insertions, 5 deletions
diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application index 1a9078994..53df6a927 100755 --- a/contrib/run-script-smtcomp2014-application +++ b/contrib/run-script-smtcomp2014-application @@ -14,12 +14,13 @@ if [ -z "$logic" ]; then echo 'ERROR: second line supposed to be set-logic, but got: "'"$line"'"' >&2 exit 1 fi +echo success function runcvc4 { # we run in this way for line-buffered input, otherwise memory's a # concern (plus it mimics what we'll end up getting from an # application-track trace runner?) - (echo "(set-logic $logic)"; cat) | $cvc4 -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@" + $cvc4 --force-logic="$logic" -L smt2 --print-success --no-checking --no-interactive --tear-down-incremental "$@" <&0- } case "$logic" in diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 0cec616fd..d9b9694e5 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -444,6 +444,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } #ifdef CVC4_COMPETITION_MODE + *opts[options::out] << flush; // exit, don't return (don't want destructors to run) // _exit() from unistd.h doesn't run global destructors // or other on_exit/atexit stuff. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 63179cf42..ba9239963 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1555,12 +1555,12 @@ symbol[std::string& id, PARSER_STATE->checkDeclaration(id, check, type); } } - | UNTERMINATED_QUOTED_SYMBOL + /*| UNTERMINATED_QUOTED_SYMBOL ( EOF { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); } | '\\' { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| symbol"); } - ) + )*/ ; /** @@ -1801,9 +1801,9 @@ EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; QUOTED_SYMBOL : '|' ~('|' | '\\')* '|' ; -UNTERMINATED_QUOTED_SYMBOL +/*UNTERMINATED_QUOTED_SYMBOL : '|' ~('|' | '\\')* - ; + ;*/ /** * Matches a keyword from the input. A keyword is a simple symbol prefixed |