From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 22 Jun 2014 06:51:31 +0000 (-0400)
Subject: Final fixes for smtcomp2014-application.
X-Git-Tag: cvc5-1.0.0~6700^2~9
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=19f565aabe8ece904f67e1353ec67a5bf485fc97;p=cvc5.git

Final fixes for smtcomp2014-application.
---

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