Regression Test : reusing LRA summary aborted
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
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).