diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-09-06 11:45:15 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-09-06 11:45:15 -0700 |
| commit | 0568888a48ab4424d3e5a166b3088db3557b9bd4 (patch) | |
| tree | b387462d8d874591e9066069c0fd7172d767d680 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
| parent | e6df57b830b1692f0968d3f3ccafb942c6f6f1e7 (diff) | |
Support multi-dimensional arrays in SMTLib2 backend (using Z3 extension though)
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 34a8502a..e8270787 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -100,10 +100,12 @@ namespace Microsoft.Boogie.SMTLib } else {
if (t.IsMap && CommandLineOptions.Clo.UseArrayTheory) {
MapType m = t.AsMap;
- Contract.Assert(m.MapArity == 1);
+ // Contract.Assert(m.MapArity == 1);
sb.Append("(Array ");
- TypeToStringHelper(m.Arguments[0], sb);
- sb.Append(" ");
+ foreach (Type tp in m.Arguments) {
+ TypeToStringHelper(tp, sb);
+ sb.Append(" ");
+ }
TypeToStringHelper(m.Result, sb);
sb.Append(")");
} else if (t.IsMap) {
|