diff options
| author |  schaef <unknown> | 2009-12-18 13:41:32 +0000 |
|---|---|---|
| committer | schaef <unknown> | 2009-12-18 13:41:32 +0000 |
| commit | d5f09caee2ca7395d0a3dae6c29d7d10a6bc1de9 (patch) | |
| tree | ca6bc4de686a6e14cc32971483a1e675ef7c5315 /Test/doomed | |
| parent | 9447617aefbe9706b0d74a827181976e4b9e9d26 (diff) | |
Doomed checking now uses the counterexample trace to minimize the number of theorem prover calls (See useCE in notdoomed.bpl).
Diffstat (limited to 'Test/doomed')
| -rw-r--r-- | Test/doomed/doomed.bpl | 4 | ||||
| -rw-r--r-- | Test/doomed/notdoomed.bpl | 18 |
2 files changed, 21 insertions, 1 deletions
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl index 77eec249..741a54c5 100644 --- a/Test/doomed/doomed.bpl +++ b/Test/doomed/doomed.bpl @@ -21,7 +21,9 @@ procedure evilbranch(x:int) } else {
y := 2;
}
- assert y!=2;
+ assume y!=2;
+
+ assert x<0;
}
diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl index eb60536f..c3193a01 100644 --- a/Test/doomed/notdoomed.bpl +++ b/Test/doomed/notdoomed.bpl @@ -35,5 +35,23 @@ procedure c(x:int) }
}
+procedure useCE(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+ if(x<7) {
+ y := 5;
+ } else {
+ y := 6;
+ }
+
+}
+
+
|