diff options
| author |  MichalMoskal <unknown> | 2011-01-19 20:50:41 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-01-19 20:50:41 +0000 |
| commit | 61c4a3d9a4fd9a4d6eb3fbb5d09f59f7efdbbaed (patch) | |
| tree | 5364aa36aeadb9f1d3fdb2dcd8b5c679c97da4bb /Source/Provers/TPTP/TPTPLineariser.cs | |
| parent | 89c7e2417ad2cf0b0cd60e5b7d46079021d88a6b (diff) | |
Fix a bug in distinct() encoding
Diffstat (limited to 'Source/Provers/TPTP/TPTPLineariser.cs')
| -rw-r--r-- | Source/Provers/TPTP/TPTPLineariser.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/TPTP/TPTPLineariser.cs b/Source/Provers/TPTP/TPTPLineariser.cs index 3e3e5ed2..cc4f8060 100644 --- a/Source/Provers/TPTP/TPTPLineariser.cs +++ b/Source/Provers/TPTP/TPTPLineariser.cs @@ -549,7 +549,7 @@ void ObjectInvariant() wr.Write("($true ");
foreach (VCExpr e in node) {
for (var i = 0; i < bits; ++i) {
- var neg = (cnt & (1 >> i)) != 0 ? "~" : "";
+ var neg = (cnt & (1 << i)) != 0 ? "~" : "";
wr.Write(" & {0}distinct__f__{1}(", neg, i);
ExprLineariser.LineariseAsTerm(e, options);
wr.Write(")");
|