Project

General

Profile

Actions
Copy link

Bug #5720

open

Regression Test : reusing LRA summary aborted

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

Status:
Resolved
Priority:
High
Assignee:
Martin Blicha
Start date:
20/10/2017
Due date:
% Done:

100%

Estimated time:

Description

When verifying the attached C code with LRA, the summary is generated successfully, but cannot be reused in the second run.

How to run:

./hifrog --claim 1 --logic qflra getchar1.c

Error message:

Assertion failed: ("Error: Not all arguments of a summary of a function was instantiated." && symbols.size() == args_instantiated), function substitute, file solvers/smt_itp.cpp, line 326.
Abort trap: 6

P.S. with the logic prop it works fine.(summary is generated and can be reused successfully).

Files

Download all files
getchar1.c (526 Bytes) getchar1.c C code Sepideh Asadi, 20/10/2017 02:39
__summaries (3.51 KB) __summaries Summary in LRA Sepideh Asadi, 20/10/2017 02:41
Actions
Copy link
 #1

Updated by Martin Blicha about 7 years ago

  • Assignee set to Martin Blicha
Actions
Copy link
 #2

Updated by Karine Even Mendoza about 7 years ago

It is very clear what is the error: "Error: Not all arguments of a summary of a function was instantiated"

Why not first fixing the writing?

Actions
Copy link
 #3

Updated by Martin Blicha about 7 years ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 100

Writing and reading of summaries is now fixed and merged into the master branch.

Actions
Copy link

Also available in: Atom PDF