diff options
| author |  Unknown <afd@afd-THINK.home> | 2012-04-09 10:31:35 +0100 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.home> | 2012-04-09 10:31:35 +0100 |
| commit | 4f521af3552c66fb79971b2d542f6b7d69d9d5f0 (patch) | |
| tree | 78bef0838399797728b5e090eb67c13122fc56be /Source | |
| parent | 0266ecb69bcb43ac37a25ae48ab21583e11a6e05 (diff) | |
Tweak to inference.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/GPUVerify/LoopInvariantGenerator.cs | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs index 7dafe20c..f61e8ef4 100644 --- a/Source/GPUVerify/LoopInvariantGenerator.cs +++ b/Source/GPUVerify/LoopInvariantGenerator.cs @@ -189,13 +189,16 @@ namespace GPUVerify if (verifier.ContainsNamedVariable(GetModifiedVariables(wc.Body), basicName))
{
verifier.AddCandidateInvariant(wc, MakePowerOfTwoExpr(v));
- for (int i = (1 << 30); i > 0; i >>= 1)
+ for (int i = (1 << 15); i > 0; i >>= 1)
{
verifier.AddCandidateInvariant(wc,
GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT",
new IdentifierExpr(v.tok, v),
new LiteralExpr(v.tok, BigNum.FromInt(i), 32)));
}
+ verifier.AddCandidateInvariant(wc,
+ Expr.Neq(new IdentifierExpr(v.tok, v),
+ new LiteralExpr(v.tok, BigNum.FromInt(0), 32)));
}
}
}
@@ -205,7 +208,7 @@ namespace GPUVerify private Expr MakePowerOfTwoExpr(Variable v)
{
Expr result = null;
- for (int i = 1 << 30; i > 0; i >>= 1)
+ for (int i = 1 << 15; i > 0; i >>= 1)
{
Expr eq = Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(i), 32));
result = (result == null ? eq : Expr.Or(eq, result));
|