summaryrefslogtreecommitdiff
path: root/src/parser/cvc/Cvc.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/cvc/Cvc.g')
-rw-r--r--src/parser/cvc/Cvc.g18
1 files changed, 11 insertions, 7 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index b496aa91c..22459037d 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -619,18 +619,22 @@ mainCommand[CVC4::Command*& cmd]
| QUERY_TOK formula[f] { cmd = new QueryCommand(f); }
| CHECKSAT_TOK formula[f] { cmd = new CheckSatCommand(f); }
- | CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
+ | CHECKSAT_TOK { cmd = new CheckSatCommand(); }
/* options */
| OPTION_TOK
( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
- symbolicExpr[sexpr]
- { if(s == "logic") {
- cmd = new SetBenchmarkLogicCommand(sexpr.getValue());
- } else {
- cmd = new SetOptionCommand(s, sexpr);
+ ( symbolicExpr[sexpr]
+ { if(s == "logic") {
+ cmd = new SetBenchmarkLogicCommand(sexpr.getValue());
+ } else {
+ cmd = new SetOptionCommand(s, sexpr);
+ }
}
- }
+ | TRUE_TOK { cmd = new SetOptionCommand(s, SExpr("true")); }
+ | FALSE_TOK { cmd = new SetOptionCommand(s, SExpr("false")); }
+ | { cmd = new SetOptionCommand(s, SExpr("true")); }
+ )
/* push / pop */
| PUSH_TOK ( k=numeral { cmd = REPEAT_COMMAND(k, PushCommand()); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback