diff options
| author |  MichalMoskal <unknown> | 2011-02-17 22:15:46 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-17 22:15:46 +0000 |
| commit | 04595976af73e34f31c529b40f0761adbc6f3902 (patch) | |
| tree | f1558eb621cbfcaf1f8ebfad7c6b98f07bf30177 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
| parent | 5a35f0c711586f03613b5d1414bd26ade65b47c5 (diff) | |
Use explicit mechanism for skipping to the next assertion
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 7df58b9e..8389ed50 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -477,11 +477,18 @@ namespace Microsoft.Boogie.SMTLib if (ExprLineariser.ProverOptions.UseLabels) {
// Z3 extension
wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));
- ExprLineariser.Linearise(node[0], options);
- wr.Write(")");
- } else {
- ExprLineariser.Linearise(node[0], options);
}
+
+ if (!op.pos)
+ wr.Write("(or {0} ", SMTLibNamer.QuoteId(SMTLibNamer.BlockedLabel(op.label)));
+
+ ExprLineariser.Linearise(node[0], options);
+
+ if (!op.pos) wr.Write(")");
+
+ if (ExprLineariser.ProverOptions.UseLabels)
+ wr.Write(")");
+
return true;
}
|