Project

General

Profile

Actions
Copy link

Bug #2307

open

Inconsistent handling of bitshifts in interpolator and solvers

Added by Pavel Shved almost 13 years ago. Updated almost 13 years ago.

Status:
Resolved
Priority:
Normal
Assignee:
Pavel Shved
Category:
-
Target version:
2.7.1
Start date:
01/27/2012
Due date:
% Done:

0%

Estimated time:
Detected in build:
2.7.1-rc1
Platform:
Published in build:

Description

When BLAST converts predicates to "FOCI" format (for instance, when interacting with the CSIsat interpolating prover), it turns bitshifts-by-constant to multiplications. See convertExpFoci in theoremProver.ml. However, when a formula is converted to the SMTlib format, such transformation does not happen.

This inconsistency prevents spurious error traces from being ruled out.

Here's a small safe program that throws NoNewPredicates. Run pblast.opt x.c with version 2.7.1.

Files

x.c (132 Bytes) x.c small file that demonstrates the problem Pavel Shved, 01/27/2012 01:04 AM

Related issues 1 (1 open — 0 closed)

Blocks BLAST - Bug #2287: cdc_eem.ko had correct unsafe verdict and became unknown in BLAST 2.7.1OpenPavel Shved01/25/2012

Actions
Actions
Copy link
 #1

Updated by Pavel Shved almost 13 years ago

forgot to attach this.

TODO: make a regression test!

Actions
Copy link
 #2

Updated by Pavel Shved almost 13 years ago

  • Status changed from New to Resolved
  • Assignee set to Pavel Shved
  • Target version set to 2.7.1
  • Detected in build changed from 2.7.1 to 2.7.1-rc1

Fixed in c1103fa; will be included into 2.7.1 release.

Actions
Copy link

Also available in: Atom PDF