hifrog

./hifrog --claim 2 ~/dev/hi-bench/main-bench/Funfrog15_bench/mem.c --logic prop

hifrog: solvers/prop_itp.cpp:366: void prop_itpt::generalize(const prop_conv_solvert&, const std::vector<symbol_exprt>&): Assertion `renaming[idx] != (0x7fffffff * 2U + 1U)' failed.
Aborted (core dumped)

Program received signal SIGABRT, Aborted.
0x00007ffff6880c37 in GI_raise (sig=sig@entry=6)
at ../nptl/sysdeps/unix/sysv/linux/raise.c:56
56 ../nptl/sysdeps/unix/sysv/linux/raise.c: No such file or directory.
(gdb) bt
#0 0x00007ffff6880c37 in _GI_raise (sig=sig@entry=6)
at ../nptl/sysdeps/unix/sysv/linux/raise.c:56
#1 0x00007ffff6884028 in __GI_abort () at abort.c:89
#2 0x00007ffff6879bf6 in __assert_fail_base (
fmt=0x7ffff69ca3b8 "%s%s%s:%u: s%sAssertion `%s' failed.\n%n",
assertion=assertion@entry=0x81ba88 "renaming[idx] != (0x7fffffff * 2U + 1U)",
file=file@entry=0x81b9d7 "solvers/prop_itp.cpp", line=line@entry=366,
function=function@entry=0x81bbc0 <prop_itpt::generalize(prop_conv_solvert constx%x, std::vector<symbol_exprt, std::allocator<symbol_exprt> > const&)::_PRETTY_FUNCTION__> "void prop_itpt::generalize(const prop_conv_solvert&, const std::vector<symbol_exprt>&)") at assert.c:92
#3 0x00007ffff6879ca2 in _GI_assert_fail (
assertion=0x81ba88 "renaming[idx] != (0x7fffffff * 2U + 1U)",
file=0x81b9d7 "solvers/prop_itp.cpp", line=366,
function=0x81bbc0 <prop_itpt::generalize(prop_conv_solvert const&, std::vector<symbol_exprt, std::allocator<symbol_exprt> > const&)::_PRETTY_FUNCTION__> "void prop_itpt::generalize(const prop_conv_solvert&, const std::vector<symbol_exprt>&)")
at assert.c:101
#4 0x00000000005a0c31 in prop_itpt::generalize (this=0x21321b0, decider=...,
symbols=std::vector of length 108, capacity 110 = {...})
at solvers/prop_itp.cpp:366
#5 0x00000000004efd96 in prop_partitioning_target_equationt::extract_interpolants (
this=0x7fffffffb970, interpolator=..., decider=...,
interpolant_map=std::vector of length 0, capacity 1)
at prop_partitioning_target_equation.cpp:726