diff options
author | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-10 16:41:36 +0100 |
---|---|---|
committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-10 16:41:36 +0100 |
commit | 2752b4bd413d5397d20331a3b8111b9abd661262 (patch) | |
tree | 14f18946d79b8c55fb2e56f00f5d626be770cd69 /Source | |
parent | 0f9de25932ded17ef7b1f52e8385274b058d901e (diff) |
fix a bug when parsing nested arrays under CVC4
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Model/ModelParser.cs | 3 |
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] == ")") |