Project

General

Profile

Bug #3489

Assertion failure when OpenSMT2 called as a library through HiFrog/master

Added by Antti Hyvärinen over 3 years ago. Updated over 3 years ago.

Status:
Closed
Priority:
Normal
Start date:
06/09/2016
Due date:
% Done:

100%

Estimated time:

Description

When running HiFrog on the example rec.c (attached).

evolcheck: PGInterAux.C:210: opensmt::icolor_t ProofGraph::getClauseColor(const ipartitions_t&, const ipartitions_t&): Assertion `clause_in_A || clause_in_B' failed.

Program received signal SIGABRT, Aborted.
0x00007ffff68d7cc9 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 0x00007ffff68d7cc9 in _GI_raise (sig=sig@entry=6) at ../nptl/sysdeps/unix/sysv/linux/raise.c:56
#1 0x00007ffff68db0d8 in __GI_abort () at abort.c:89
#2 0x00007ffff68d0b86 in __assert_fail_base (fmt=0x7ffff6a223d0 "%s%s%s:%u: s%sAssertion `%s' failed.\n%n", assertion=assertion@entry=0x7ffff7b699d5 "clause_in_A || clause_in_B", file=file@entry=0x7ffff7b698cb "PGInterAux.C", line=line@entry=210,
function=function@entry=0x7ffff7b69f20 <ProofGraph::getClauseColor(
_gmp_expr<__mpz_struct [1], _mpz_struct [1]> constx%x, __gmp_expr<_mpz_struct [1], _mpz_struct [1]> const&)::_PRETTY_FUNCTION__> "opensmt::icolor_t ProofGraph::getClauseColor(const ipartitions_t&, const ipartitions_t&)") at assert.c:92
#3 0x00007ffff68d0c32 in _GI
_assert_fail (assertion=0x7ffff7b699d5 "clause_in_A || clause_in_B", file=0x7ffff7b698cb "PGInterAux.C", line=210,
function=0x7ffff7b69f20 <ProofGraph::getClauseColor(
_gmp_expr<__mpz_struct [1], _mpz_struct [1]> const&, __gmp_expr<_mpz_struct [1], _mpz_struct [1]> const&)::_PRETTY_FUNCTION__> "opensmt::icolor_t ProofGraph::getClauseColor(const ipartitions_t&, const ipartitions_t&)") at assert.c:101
#4 0x00007ffff7b26e16 in ProofGraph::getClauseColor (this=0x1358d50, clause_mask=..., A_mask=...) at PGInterAux.C:210
#5 0x00007ffff7b30864 in ProofGraph::produceSingleInterpolant (this=0x1358d50, interpolants=..., A_mask=...) at PGInterpolator.C:435
#6 0x00007ffff7a9cb75 in CoreSMTSolver::getSingleInterpolant (this=0x169e180, interpolants=..., A_mask=...) at Proof.C:626
#7 0x0000000000591608 in CoreSMTSolver::getSingleInterpolant (this=0x169e180, interpolants=..., A_mask=...) at /home/hyvaeria/opensmt2-install/include/opensmt/CoreSMTSolver.h:914
#8 0x0000000000590217 in satcheck_opensmt2t::produceConfigMatrixInterpolants (this=0x1e65210, configs=..., interpolants=...) at solvers/satcheck_opensmt2.cpp:164
#9 0x0000000000590369 in satcheck_opensmt2t::get_interpolant (this=0x1e65210, partition_ids=..., interpolants=...) at solvers/satcheck_opensmt2.cpp:198
#10 0x000000000042775a in partitioning_target_equationt::extract_interpolants (this=0x7fffffffc680, interpolator=..., decider=..., interpolant_map=...) at partitioning_target_equation.cpp:833
#11 0x000000000048304a in summarizing_checkert::extract_interpolants (this=0x7fffffffd720, prop=..., equation=...) at summarizing_checker.cpp:212
#12 0x00000000004824f4 in summarizing_checkert::assertion_holds (this=0x7fffffffd720, assertion=..., store_summaries_with_assertion=false) at summarizing_checker.cpp:140
#13 0x0000000000450dbe in check_claims (ns=..., leaping_program=..., goto_functions=..., claim_map=..., claim_numbers=..., options=..., _message_handler=..., claim_nr=0) at check_claims.cpp:211
#14 0x000000000044a9ff in funfrog_parseoptionst::check_function_summarization (this=0x7fffffffe2b0, ns=..., goto_functions=...) at parseoptions.cpp:562
#15 0x0000000000449beb in funfrog_parseoptionst::doit (this=0x7fffffffe2b0) at parseoptions.cpp:312
#16 0x00000000007c10dc in parseoptions_baset::main (this=0x7fffffffe2b0) at parseoptions.cpp:104
#17 0x000000000048c96d in main (argc=2, argv=0x7fffffffea48) at main.cpp:36

rec.c (219 Bytes) rec.c Antti Hyvärinen, 06/09/2016 09:53

History

#1 Updated by Antti Hyvärinen over 3 years ago

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

Also available in: Atom PDF