Final fixes for smtcomp2014-application.

diff --git a/contrib/run-script-smtcomp2014-application b/contrib/run-script-smtcomp2014-application
index 1a9078994fb8a4f3da98f39eaf26ac416627e833..53df6a927cefd22e9569ad04dc657daa5e519394 100755 (executable)
--- 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 0cec616fdcfdc83d47b1f33ee8ad202b00ae4b02..d9b9694e5c986265d55d166bbf84efca401cfe51 100644 (file)
--- 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 63179cf42467c490368954edbf37f92af6e05d89..ba9239963c0ded97e67c3f04c7837e5b99e4f84a 100644 (file)
--- 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