summaryrefslogtreecommitdiff
path: root/src/parser/cvc
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-10-04 01:25:35 +0000
committerMorgan Deters <mdeters@gmail.com>2011-10-04 01:25:35 +0000
commit87ea8ded0593debfda9d649bcce086286247c9fd (patch)
treeefb863e5f6b81f375926e52f7e8dd8fdecd7318e /src/parser/cvc
parent09f28a6a107e2599c2f53d1dd8d201d8c18e625f (diff)
Oh, here's another cute compatibility fix for libantlr3c 3.4-beta4. They #define true and false to their own ANTLR3_TRUE and ANTLR3_FALSE, wreaking havoc on our parsers. I'm really fed up with this package.
Diffstat (limited to 'src/parser/cvc')
-rw-r--r--src/parser/cvc/Cvc.g6
1 files changed, 3 insertions, 3 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback