summaryrefslogtreecommitdiff
path: root/Source/Model
diff options
context:
space:
mode:
authorGravatar Pantazis Deligiannis <pdeligia@me.com>2013-07-10 16:41:36 +0100
committerGravatar Pantazis Deligiannis <pdeligia@me.com>2013-07-10 16:41:36 +0100
commit2752b4bd413d5397d20331a3b8111b9abd661262 (patch)
tree14f18946d79b8c55fb2e56f00f5d626be770cd69 /Source/Model
parent0f9de25932ded17ef7b1f52e8385274b058d901e (diff)
fix a bug when parsing nested arrays under CVC4
Diffstat (limited to 'Source/Model')
-rw-r--r--Source/Model/ModelParser.cs3
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs
index 5de903ab..0a7a6c69 100644
--- a/Source/Model/ModelParser.cs
+++ b/Source/Model/ModelParser.cs
@@ -681,6 +681,9 @@ namespace Microsoft.Boogie
if (tokens [i] == "(" && tokens [i + 1] == "__array_store_all__") {
output.Add ("as-array[k!" + arrayNum + "]");
SplitArrayExpression ();
+ } else if (tokens [i] == "(" && tokens [i + 1] == "store") {
+ output.Add ("as-array[k!" + arrayNum + "]");
+ SplitArrayExpression ();
} else {
while (args.Count < 3) {
if (tokens [i] == ")")