Project

General

Profile

Actions

Bug #5519

open

Function summary + UF/LRA does not work

Added by Sepideh Asadi about 7 years ago. Updated about 7 years ago.

Status:
Resolved
Priority:
High
Start date:
13/08/2017
Due date:
% Done:

90%

Estimated time:
Spent time:

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.

Actions #1

Updated by Karine Even Mendoza about 7 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

Actions

Also available in: Atom PDF