Project

General

Profile

Bug #5720

Regression Test : reusing LRA summary aborted

Added by Sepideh Asadi over 6 years ago. Updated over 6 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).

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

History

#1 Updated by Martin Blicha over 6 years ago

  • Assignee set to Martin Blicha

#2 Updated by Karine Even Mendoza over 6 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?

#3 Updated by Martin Blicha over 6 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.

Also available in: Atom PDF