Project

General

Profile

Actions
Copy link

Bug #2699

open

BLAST doesn't find an error in a rather simple example with division

Added by Evgeny Novikov about 12 years ago. Updated about 12 years ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Target version:
-
Start date:
04/04/2012
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

CPAchecker finds it. The example with description in attachment.
In fact the example is a minimal test case (I guess) for a real driver that is also attached. On that driver BLAST quickly fails with the same error, while CPAchecker is killed because of time out of 15 minutes.

Files

Download all files
test.c (330 Bytes) test.c Example with division that fails BLAST Evgeny Novikov, 04/04/2012 03:04 PM
drivers-usb-class-cdc-acm.o.general.i (1.54 MB) drivers-usb-class-cdc-acm.o.general.i Real driver that has the same problem Evgeny Novikov, 04/04/2012 03:04 PM
Actions
Copy link
 #1

Updated by Pavel Shved about 12 years ago

CSIsat interpolating prover doesn't seem to support division. BLAST replaces the division by an uninterpreted function. So it can reason that if a==b then a/2 b/2, but it can't deduce that a1 from a1==2 && a==a1/2. CVC3, however, solves this correctly, and causes the SAT error.

Actions
Copy link

Also available in: Atom PDF