Project

General

Profile

Actions
Copy link

Bug #2037

open

Interpolants with disjunctions are broke down into unusable chunks even in smaller programs

Added by Pavel Shved over 12 years ago. Updated over 12 years ago.

Status:
New
Priority:
Normal
Assignee:
Pavel Shved
Category:
-
Target version:
-
Start date:
11/26/2011
Due date:
% Done:

0%

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

Description

It seems that I broke something in new SMT useful-block algorithm, and this very simple program is not verified correctly (throws NoNewPredicates exception).

for (i=0; i<2; i++){
  ox = i;
}
if (ox != 1) err();

I added a similar test in b80e6ef.

Actions
Copy link
 #1

Updated by Pavel Shved over 12 years ago

  • Subject changed from A simple loop program is not verified correctly to Interpolants with disjunctions are broke down into unusable chunks even in smaller programs
  • Priority changed from Urgent to Normal
  • Target version deleted (2.7.1)

During the last step in the loop analysis, the following are detected as useful blocks (i0 is a SSA-indexed version of i):

1: (pre-state) i0 <= 1
2:    block    ox = i0
3:             i = i0 + 1
4:    pred     i >= 2
5:    pred     ox != 1

Though it may sound tricky, this set is unsat. Conjuncts (1), (3) and (4) imply that i0 is equal to one. This implies that ox is equal to 1. Since the assignment to ox is "wrapped" into the conjuncts that make its value known, the interpolant between (3) and (4) will be tricky here. It is

(i >= 2) implies (ox = 1)

Since it's basically a disjunction, it's broke down into two "atomic" predicates, (i0 => 2) and (ox = 1), which are tracked separately. No wonder that their disjunction is never enforced.

Since it's a known bug in BLAST, and it was not caused by the recent enhancements (and, perhaps, there is an option to prevent this smashing), lowering priority.

By the way, loop has nothing to do with this either.

Actions
Copy link

Also available in: Atom PDF