diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-24 12:24:31 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-09-24 12:24:31 +0100 |
| commit | 8ce0d761f21e4449d9fff832601352f390e26f49 (patch) | |
| tree | 5ff42a50fc9cac438ce01322217e75b93624a57a /Source/Provers/SMTLib/SExpr.cs | |
| parent | 716dc807128ac5bed97b22af0144ef516a3721e5 (diff) | |
Let the SMT lib convert models to Z3-like models
The Model parser for SMT models is broken beyond repair
and this by-passes this. The code could be moved to the
model parser, but that's a refactoring for another day.
Also, the existing version already had multiple reparses
going on and this at least removes one of those.
Patch by Jeroen Ketema.
Diffstat (limited to 'Source/Provers/SMTLib/SExpr.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SExpr.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SExpr.cs b/Source/Provers/SMTLib/SExpr.cs index ba07ec27..ac681b8a 100644 --- a/Source/Provers/SMTLib/SExpr.cs +++ b/Source/Provers/SMTLib/SExpr.cs @@ -89,6 +89,8 @@ namespace Microsoft.Boogie if (Arguments.Length > 0) sb.Append('(');
if (Name.Any(Char.IsWhiteSpace))
sb.Append("\"").Append(Name).Append("\"");
+ else if (Name.Length == 0)
+ sb.Append("()");
else
sb.Append(Name);
foreach (var a in Arguments) {
|