diff options
| author |  Ally Donaldson <unknown> | 2013-07-22 19:12:40 +0100 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-07-22 19:12:40 +0100 |
| commit | eea0a9e74d6782d08f8dd01c0e1dbec15f1a02cb (patch) | |
| tree | 26b5693006a283d80fb47507263e404c282ae2ef /Source/Provers/SMTLib | |
| parent | 62d2fa72d5e1816d6cb1239063302808424c6d13 (diff) | |
More refactoring
Diffstat (limited to 'Source/Provers/SMTLib')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 7fffd6fc..4e94c238 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -273,7 +273,7 @@ namespace Microsoft.Boogie.SMTLib foreach (Function f in ctx.KnownDatatypeConstructors[datatype])
{
string quotedConstructorName = Namer.GetQuotedName(f, f.Name);
- if (f.InParams.Length == 0)
+ if (f.InParams.Count == 0)
{
datatypeString += quotedConstructorName + " ";
}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 2bbe4978..2bf8fa22 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -209,7 +209,7 @@ void ObjectInvariant() string printedName = Namer.GetQuotedName(f, f.Name);
Contract.Assert(printedName != null);
- Contract.Assert(f.OutParams.Length == 1);
+ Contract.Assert(f.OutParams.Count == 1);
var argTypes = f.InParams.Cast<Variable>().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " ");
string decl;
if(RegisteredRelations.Contains(op.Func))
|