USI & SUPSI Source Code Management (SCM): Issueshttps://scm.ti-edu.ch/https://scm.ti-edu.ch/favicon.ico?15601711372016-09-06T07:53:59ZUSI & SUPSI Source Code Management (SCM)
Redmine OpenSMT 2 - Bug #3489 (Closed): Assertion failure when OpenSMT2 called as a library through HiFro...https://scm.ti-edu.ch/issues/34892016-09-06T07:53:59ZAntti HyvärinenAntti.Hyvarinen@gmail.com
<p>When running HiFrog on the example rec.c (attached).</p>
<p>evolcheck: PGInterAux.C:210: opensmt::icolor_t ProofGraph::getClauseColor(const ipartitions_t&, const ipartitions_t&): Assertion `clause_in_A || clause_in_B' failed.</p>
<p>Program received signal SIGABRT, Aborted.<br />0x00007ffff68d7cc9 in <i>GI_raise (sig=sig@entry=6) at ../nptl/sysdeps/unix/sysv/linux/raise.c:56<br />56 ../nptl/sysdeps/unix/sysv/linux/raise.c: No such file or directory.<br />(gdb) bt<br />#0 0x00007ffff68d7cc9 in _<em>GI_raise (sig=sig@entry=6) at ../nptl/sysdeps/unix/sysv/linux/raise.c:56<br />#1 0x00007ffff68db0d8 in __GI_abort () at abort.c:89<br />#2 0x00007ffff68d0b86 in __assert_fail_base (fmt=0x7ffff6a223d0 "%s%s%s:%u: <span>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,<br /> function=function@entry=0x7ffff7b69f20 <ProofGraph::getClauseColor(</em>_gmp_expr<__mpz_struct [1], _<em>mpz_struct [1]> constx%x</span>, __gmp_expr<</em>_mpz_struct [1], _<em>mpz_struct [1]> const&)::</em>_PRETTY_FUNCTION__> "opensmt::icolor_t ProofGraph::getClauseColor(const ipartitions_t&, const ipartitions_t&)") at assert.c:92<br />#3 0x00007ffff68d0c32 in _<em>GI</i>_assert_fail (assertion=0x7ffff7b699d5 "clause_in_A || clause_in_B", file=0x7ffff7b698cb "PGInterAux.C", line=210,<br /> function=0x7ffff7b69f20 <ProofGraph::getClauseColor(</em>_gmp_expr<__mpz_struct [1], _<em>mpz_struct [1]> const&, __gmp_expr<</em>_mpz_struct [1], _<em>mpz_struct [1]> const&)::</em>_PRETTY_FUNCTION__> "opensmt::icolor_t ProofGraph::getClauseColor(const ipartitions_t&, const ipartitions_t&)") at assert.c:101<br />#4 0x00007ffff7b26e16 in ProofGraph::getClauseColor (this=0x1358d50, clause_mask=..., A_mask=...) at PGInterAux.C:210<br />#5 0x00007ffff7b30864 in ProofGraph::produceSingleInterpolant (this=0x1358d50, interpolants=..., A_mask=...) at PGInterpolator.C:435<br />#6 0x00007ffff7a9cb75 in CoreSMTSolver::getSingleInterpolant (this=0x169e180, interpolants=..., A_mask=...) at Proof.C:626<br />#7 0x0000000000591608 in CoreSMTSolver::getSingleInterpolant (this=0x169e180, interpolants=..., A_mask=...) at /home/hyvaeria/opensmt2-install/include/opensmt/CoreSMTSolver.h:914<br />#8 0x0000000000590217 in satcheck_opensmt2t::produceConfigMatrixInterpolants (this=0x1e65210, configs=..., interpolants=...) at solvers/satcheck_opensmt2.cpp:164<br />#9 0x0000000000590369 in satcheck_opensmt2t::get_interpolant (this=0x1e65210, partition_ids=..., interpolants=...) at solvers/satcheck_opensmt2.cpp:198<br />#10 0x000000000042775a in partitioning_target_equationt::extract_interpolants (this=0x7fffffffc680, interpolator=..., decider=..., interpolant_map=...) at partitioning_target_equation.cpp:833<br />#11 0x000000000048304a in summarizing_checkert::extract_interpolants (this=0x7fffffffd720, prop=..., equation=...) at summarizing_checker.cpp:212<br />#12 0x00000000004824f4 in summarizing_checkert::assertion_holds (this=0x7fffffffd720, assertion=..., store_summaries_with_assertion=false) at summarizing_checker.cpp:140<br />#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<br />#14 0x000000000044a9ff in funfrog_parseoptionst::check_function_summarization (this=0x7fffffffe2b0, ns=..., goto_functions=...) at parseoptions.cpp:562<br />#15 0x0000000000449beb in funfrog_parseoptionst::doit (this=0x7fffffffe2b0) at parseoptions.cpp:312<br />#16 0x00000000007c10dc in parseoptions_baset::main (this=0x7fffffffe2b0) at parseoptions.cpp:104<br />#17 0x000000000048c96d in main (argc=2, argv=0x7fffffffea48) at main.cpp:36</p> OpenSMT 2 - Bug #3488 (Resolved): SIGSEGV in LRASolverhttps://scm.ti-edu.ch/issues/34882016-09-06T07:48:15ZAntti HyvärinenAntti.Hyvarinen@gmail.com
<p>The following stack trace appears when running the example rec.c (attached)</p>
<p>Program received signal SIGSEGV, Segmentation fault.<br />0x00007ffff7a54750 in LAVar::U (this=0x0) at LAVar.h:284<br />284 assert( all_bounds[u_bound].delta );<br />(gdb) bt<br />#0 0x00007ffff7a54750 in LAVar::U (this=0x0) at LAVar.h:284<br />#1 0x00007ffff7a66411 in LAVar::isModelOutOfBounds (this=0x0) at LAVar.h:184<br />#2 0x00007ffff7a59947 in LRASolver::check (this=0x1af86d0, complete=false) at LRASolver.C:458<br />#3 0x00007ffff7a4a33a in TSolverHandler::check (this=0x1e07420, complete=false) at TSolverHandler.C:80<br />#4 0x00007ffff7a43652 in THandler::check (this=0x207d0f0, complete=false) at THandler.C:132<br />#5 0x00007ffff7abd382 in CoreSMTSolver::checkTheory (this=0x1aac0e0, complete=false) at Theory.C:91<br />#6 0x00007ffff7ab1138 in CoreSMTSolver::search (this=0x1aac0e0, nof_conflicts=100, nof_learnts=29) at CoreSMTSolver.C:1863<br />#7 0x00007ffff7ab325b in CoreSMTSolver::solve_ (this=0x1aac0e0, max_conflicts=0) at CoreSMTSolver.C:2424<br />#8 0x00007ffff7aa3717 in SimpSMTSolver::solve_ (this=0x1aac0e0, do_simp=false, turn_off_simp=true) at SimpSMTSolver.C:185<br />#9 0x00007ffff7b062d2 in SimpSMTSolver::solve (this=0x1aac0e0, assumps=..., do_simp=false, turn_off_simp=true) at ../../src/smtsolvers/SimpSMTSolver.h:263<br />#10 0x00007ffff7b03553 in Cnfizer::solve (this=0x170ccc8, en_frames=...) at Cnfizer.C:88<br />#11 0x00007ffff7ad1430 in MainSolver::solve (this=0x170cc90) at MainSolver.C:1090<br />#12 0x00007ffff7ad127e in MainSolver::check (this=0x170cc90) at MainSolver.C:1069<br />#13 0x0000000000589ccc in smtcheck_opensmt2t::solve (this=0xeab100) at solvers/smtcheck_opensmt2.cpp:845<br />#14 0x00000000004625f0 in prop_assertion_sumt::is_satisfiable (this=0x7fffffffc2f0, decider=...) at prop_assertion_sum.cpp:130<br />#15 0x0000000000462451 in prop_assertion_sumt::assertion_holds (this=0x7fffffffc2f0, assertion=..., ns=..., decider=..., interpolator=...) at prop_assertion_sum.cpp:51<br />#16 0x00000000004771b4 in summarizing_checkert::assertion_holds (this=0x7fffffffd700, assertion=..., store_summaries_with_assertion=false) at summarizing_checker.cpp:127<br />#17 0x0000000000455fbe in check_claims (ns=..., leaping_program=..., goto_functions=..., claim_map=..., claim_numbers=..., options=..., _message_handler=..., claim_nr=0) at check_claims.cpp:211<br />#18 0x000000000044fbff in funfrog_parseoptionst::check_function_summarization (this=0x7fffffffe2b0, ns=..., goto_functions=...) at parseoptions.cpp:562<br />#19 0x000000000044edeb in funfrog_parseoptionst::doit (this=0x7fffffffe2b0) at parseoptions.cpp:312<br />#20 0x00000000007c05dc in parseoptions_baset::main (this=0x7fffffffe2b0) at parseoptions.cpp:104<br />#21 0x000000000048079f in main (argc=2, argv=0x7fffffffea48) at main.cpp:36</p> OpenSMT 2 - Bug #3487 (Closed): Local variables appearing in LRA interpolantshttps://scm.ti-edu.ch/issues/34872016-09-06T07:38:34ZAntti HyvärinenAntti.Hyvarinen@gmail.com