diff options
| author |  wuestholz <unknown> | 2013-05-26 15:53:05 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-05-26 15:53:05 -0700 |
| commit | e6241dfdc9743cbbf3f1ae9fb61f3e3179a417f9 (patch) | |
| tree | 14ddef6c41595577c35fc8767bc56af1063ad813 /Test/prover | |
| parent | a05745053d88f93508d33eacd38c69b339a45d50 (diff) | |
Changed the 'CounterexampleComparer' to take traces into account.
Diffstat (limited to 'Test/prover')
| -rw-r--r-- | Test/prover/Answer | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/prover/Answer b/Test/prover/Answer index 1ca6407c..13621984 100644 --- a/Test/prover/Answer +++ b/Test/prover/Answer @@ -4,7 +4,7 @@ z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(14,1): L3
+ z3mutl.bpl(8,1): L1
z3mutl.bpl(20,1): L5
z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
@@ -14,7 +14,7 @@ Execution trace: z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(8,1): L1
+ z3mutl.bpl(14,1): L3
z3mutl.bpl(20,1): L5
Boogie program verifier finished with 0 verified, 3 errors
|