projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
fb51c4e
)
rm warning
author
Kshitij Bansal
<kshitij@cs.nyu.edu>
Thu, 10 Jul 2014 20:05:25 +0000
(16:05 -0400)
committer
Kshitij Bansal
<kshitij@cs.nyu.edu>
Thu, 10 Jul 2014 23:31:00 +0000
(19:31 -0400)
src/parser/smt2/Smt2.g
patch
|
blob
|
history
diff --git
a/src/parser/smt2/Smt2.g
b/src/parser/smt2/Smt2.g
index 085cc11c840ca532c6acfd428bb47c2008bdbe08..d512437af6a0266a73c0ff5d1bdda2784b44fa97 100644
(file)
--- a/
src/parser/smt2/Smt2.g
+++ b/
src/parser/smt2/Smt2.g
@@
-1206,7
+1206,7
@@
indexedFunctionName[CVC4::Expr& op]
( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
{ op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
AntlrInput::tokenToUnsigned($n2))); }
- | 'repeat' n=INTEGER_LITERAL
+ |
('repeat' INTEGER_LITERAL)=>
'repeat' n=INTEGER_LITERAL
{ op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
| 'zero_extend' n=INTEGER_LITERAL
{ op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }