Project

General

Profile

Bug #5519

Function summary + UF/LRA does not work

Added by Sepideh Asadi over 6 years ago. Updated over 6 years ago.

Status:
Resolved
Priority:
High
Assignee:
Karine Even Mendoza
Start date:
13/08/2017
Due date:
% Done:

90%

Estimated time:
Spent time:
1.00 h

Description

It seems in UF/LRA Interpolants are generated but cannot be reused.

./hifrog --logic qfuf --claim 1 --unwind 10 token.c

hifrog: solvers/smt_itp.cpp:273: void smt_itpt::substitute(smtcheck_opensmt2t&, const std::vector<symbol_exprt>&, bool) const: Assertion `aname == unidx_aname || aname.find("::#return_value!0") != string::npos' failed.
Aborted (core dumped)

----------
QF-Bool works fine.

History

#1 Updated by Karine Even Mendoza over 6 years ago

  • Status changed from New to Resolved
  • Assignee set to Karine Even Mendoza
  • % Done changed from 0 to 90

Still in private, will move with all lattice ref. recent work when we will merge with master

Also available in: Atom PDF