diff options
| author |  Ken McMillan <unknown> | 2014-02-21 12:13:20 -0800 |
|---|---|---|
| committer | Ken McMillan <unknown> | 2014-02-21 12:13:20 -0800 |
| commit | d4d59ba1cbc91160a3d15cbf615878af971448e6 (patch) | |
| tree | 653f57c4b0db1e1a1c5be37e62b0502b06c0ff41 /Source/Model | |
| parent | 570b2104a5a4ba74d0bd3d845f6625ecd5825df7 (diff) | |
Fixed crash in ModelParser when Z3 returns an operator that is a list.
Diffstat (limited to 'Source/Model')
| -rw-r--r-- | Source/Model/ModelParser.cs | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs index dc6e06b5..ded145ed 100644 --- a/Source/Model/ModelParser.cs +++ b/Source/Model/ModelParser.cs @@ -65,7 +65,9 @@ namespace Microsoft.Boogie string s = o as string; if (s != null) return GetElt (s); - List<object> os = (List<object>)o; + List<object> os = (List<object>)o;
+ if (!(os[0] is string))
+ os.Insert(0, "_"); // KLM: fix crash on ((as const (Array Int Int)) 0) List<Model.Element> args = new List<Model.Element> (); for (int i = 1; i < os.Count; i++) { args.Add (GetElt (os [i])); |