Project

General

Profile

Bug #7414

seg fault in reading non-linear elf summary in lra - sum-theoref

Added by Sepideh Asadi 11 months ago.

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

sumth73.c (897 Bytes) sumth73.c Sepideh Asadi, 24/05/2018 14:37

Also available in: Atom PDF