Bug #7414
seg fault in reading non-linear elf summary in lra - sum-theoref
Status:
In Progress
Priority:
Normal
Assignee:
-
Start date:
24/05/2018
Due date:
% Done:
0%
Estimated time:
Description
How to run: ./hifrog --sum-theoref sumth73.c (c file in attachement)
Error msg:
---EUF was not enough, lets change the encoding to LRA---
; Warning: disabling SATElite preprocessing to track proof
--Reading LRA and UF summary files: _summaries_uf,_summaries_lra
Non linear operation encounter. Ignoring 10 expressions in the file.
----Reading summary file: __summaries_uf
Non linear operation encounter in file __summaries_uf. Ignoring this file.
----Reading summary file: __summaries_lra
----Reading summary file: __summaries_linear_temp
; lra checker query time so far: 0.000000
zsh: segmentation fault ./hifrog --sum-theoref sumth73.c