diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-04-28 13:32:38 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-04-28 13:32:38 -0700 |
| commit | dfb4e6c3a65c8bf7cd95bfe27bf5a33ba0c73f3c (patch) | |
| tree | 583b8b855c384c4228ebfaa006276896c8467b02 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
| parent | 386085ef362905d564753e8e6d252540ceef0e85 (diff) | |
Use (get-model) Z3 command; quote skolem-ids
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index d06cba3b..3e8a3fc8 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -266,7 +266,7 @@ namespace Microsoft.Boogie.SMTLib if (weight != 1)
wr.Write(" :weight {0}\n", weight);
if (infos.uniqueId != -1)
- wr.Write(" :skolemid {0}\n", infos.uniqueId);
+ wr.Write(" :skolemid |{0}|\n", infos.uniqueId);
WriteTriggers(node.Triggers, options);
wr.Write(")");
|