diff options
| author |  Unknown <afd@afd-THINK.doc.ic.ac.uk> | 2012-02-08 09:16:16 +0000 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.doc.ic.ac.uk> | 2012-02-08 09:16:16 +0000 |
| commit | 2b05e5c60ab3b14919c33da76c2c46bf22c6eb92 (patch) | |
| tree | 9d68a7003003c2412b7ec277f95a20eef217fa32 /Source/GPUVerify | |
| parent | 5e1ab7bb232d11f01bcfaaf828e4b26fdc0c3f50 (diff) | |
Predicated assumes
Diffstat (limited to 'Source/GPUVerify')
| -rw-r--r-- | Source/GPUVerify/Predicator.cs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs index a4174cbb..e2af8185 100644 --- a/Source/GPUVerify/Predicator.cs +++ b/Source/GPUVerify/Predicator.cs @@ -143,6 +143,10 @@ namespace GPUVerify {
firstBigBlock.simpleCmds.Add(new AssertCmd(c.tok, Expr.Imp(IncomingPredicate, (c as AssertCmd).Expr)));
}
+ else if (c is AssumeCmd)
+ {
+ firstBigBlock.simpleCmds.Add(new AssumeCmd(c.tok, Expr.Imp(IncomingPredicate, (c as AssumeCmd).Expr)));
+ }
else
{
Debug.Assert(false);
|