diff options
-rw-r--r-- | src/parser/cvc/Cvc.g | 6 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 4 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 1f817350c..955f3a1f4 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -587,7 +587,7 @@ 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(true)); } + | CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(bool(true))); } /* options */ | OPTION_TOK @@ -1655,8 +1655,8 @@ simpleTerm[CVC4::Expr& f] } /* boolean literals */ - | TRUE_TOK { f = MK_CONST(true); } - | FALSE_TOK { f = MK_CONST(false); } + | TRUE_TOK { f = MK_CONST(bool(true)); } + | FALSE_TOK { f = MK_CONST(bool(false)); } /* arithmetic literals */ /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot! * This is a rational constant! Otherwise the parser interprets it as a tuple diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index da20c68a2..083bdf3b5 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -278,8 +278,8 @@ annotatedFormula[CVC4::Expr& expr] { PARSER_STATE->popScope(); } /* constants */ - | TRUE_TOK { expr = MK_CONST(true); } - | FALSE_TOK { expr = MK_CONST(false); } + | TRUE_TOK { expr = MK_CONST(bool(true)); } + | FALSE_TOK { expr = MK_CONST(bool(false)); } | NUMERAL_TOK { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); } | RATIONAL_TOK diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5ae04adea..f9a2cccf2 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -290,7 +290,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new AssertCommand(expr); } | /* checksat */ CHECKSAT_TOK - { cmd = new CheckSatCommand(MK_CONST(true)); } + { cmd = new CheckSatCommand(MK_CONST(bool(true))); } | /* get-assertions */ GET_ASSERTIONS_TOK { cmd = new GetAssertionsCommand; } |