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/SMTLibProcess.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/SMTLibProcess.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProcess.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 439557c0..4a1331c5 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -210,10 +210,11 @@ namespace Microsoft.Boogie.SMTLib return '\0';
}
+
while (linePos < currLine.Length && char.IsWhiteSpace(currLine[linePos]))
linePos++;
- if (linePos < currLine.Length)
+ if (linePos < currLine.Length && currLine[linePos] != ';')
return currLine[linePos];
else {
currLine = null;
|