diff options
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) {
|