Actions
Bug #5519
openFunction summary + UF/LRA does not work
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.
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