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 almost 13 years ago. Updated almost 13 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

Also available in: Atom PDF