diff options
| author |  Ally Donaldson <unknown> | 2013-12-09 09:40:27 +0000 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-12-09 09:40:27 +0000 |
| commit | c44eeb0c3120f6bd9d377019e96ea11508252806 (patch) | |
| tree | 1a842c38d83e7b1f3b854b862a3dc61e7f2cef7a /Source/Provers | |
| parent | decec0038a658079c8e54d7a1eb97795155836ce (diff) | |
Small change related to CVC4 support. Patch by Pantazis Deligiannis
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 6b4f8cb9..668dede9 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -964,8 +964,7 @@ namespace Microsoft.Boogie.SMTLib if (resp.Name == "model" && resp.ArgCount >= 1) {
modelStr = resp.Arguments[0] + "\n";
for (int i = 1; i < resp.ArgCount; i++) {
- if (resp.Arguments[i].ToString().Contains("define-fun") &&!resp.Arguments[i].ToString().Contains("not"))
- modelStr += resp.Arguments[i] + "\n";
+ modelStr += resp.Arguments[i] + "\n";
}
}
else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {
|