summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2012-07-10 01:20:44 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2012-07-10 01:20:44 +0000
commit05b9f9f137028cc072538cc37df427769fd5eace (patch)
treef4e51d4c2cd66192f667c769d1797dcde4b7c22d /src/parser
parent42e7a38f0a0b38722c2f58ff028a5d3af9337347 (diff)
small changes:
* smtlib2 decimal constant can be "1.", i.e. doesn't need digits after the point * adding CVC4_PUBLIC to rational output operator, otherwise it's unusable for users
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/smt2/Smt2.g2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 84d75ceac..2b331c58a 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1196,7 +1196,7 @@ fragment NUMERAL
* Matches a decimal constant from the input.
*/
DECIMAL_LITERAL
- : NUMERAL '.' DIGIT+
+ : NUMERAL '.' DIGIT*
;
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback