USI & SUPSI Source Code Management (SCM): Issues
https://scm.ti-edu.ch/
https://scm.ti-edu.ch/favicon.ico?1560171137
2017-05-31T07:49:46Z
USI & SUPSI Source Code Management (SCM)
Redmine
hifrog - Bug #5225 (New): SAT examples are terminate with "killed" when using the right/correct p...
https://scm.ti-edu.ch/issues/5225
2017-05-31T07:49:46Z
Karine Even Mendoza
karine.even_mendoza@kcl.ac.uk
<p>For example:<br />hi-bench/challenge-bench/sv-comp16/c/bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c --logic qfcuf --unwind 6 --no-partitions --theoref --no-itp --force --bitwidth 64</p>
<p>hi-bench/challenge-bench/sv-comp16/c/bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c --logic qfcuf --unwind 8 --no-partitions --theoref --no-itp --force --bitwidth 16</p>
<p>Two of the SAT examples I looked at. I'll try to add more if I'll find later on today.</p>
<p>Thanks!</p>
hifrog - Bug #5218 (Feedback): Wrong result in ECA with global vars for Problem01_label38_false-u...
https://scm.ti-edu.ch/issues/5218
2017-05-28T08:29:41Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>/hifrog/trunk/cprover/src/funfrog/hifrog --claim 1 --bitwidth 32 --unwind 10 --no-itp ~/hi-bench/challenge-bench/sv-comp16/c/eca-rers2012/Problem01_label38_false-unreach-call.c --logic prop<br />result with prop: <strong>UNSAT</strong>, 54 sec<br />--------------------------------------------------------</p>
<p>/hifrog/trunk/cprover/src/funfrog/hifrog --claim 1 --bitwidth 32 --unwind 10 --no-itp ~/hi-bench/challenge-bench/sv-comp16/c/eca-rers2012/Problem01_label38_false-unreach-call.c --theoref<br />Result with CUF: <strong>UNSAT</strong>, 27 sec</p>
<p>--------------------------------------------------------<br />./cbmc --unwind 10 <br />Result with CBMC: <strong>SAT</strong> , 20 sec</p>
<p>cbmc log:<br />91898 variables, 294206 clauses<br />SAT checker: instance is SATISFIABLE<br />Runtime decision procedure: 8.099s</p>
<ul>
<li>Results:<br />[calculate_output.assertion.1] : FAILURE</li>
</ul>
<ul>
<li>1 of 1 failed (1 iteration)<br />VERIFICATION FAILED<br />Command exited with non-zero status 10<br />real 20.52</li>
</ul>
hifrog - Bug #5107 (New): inconsistency in directory: product-lines
https://scm.ti-edu.ch/issues/5107
2017-05-02T18:41:21Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>HiFROG:<br />minepump_spec4_product41_false-unreach-call.cil.c UNSAT with CUSTOM 6.229 s</p>
<p>CBMC:<br />minepump_spec4_product41_false-unreach-call.cil.c SAT 1.6 s</p>
hifrog - Bug #5099 (New): prop
https://scm.ti-edu.ch/issues/5099
2017-04-28T21:35:35Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>./hifrog --claim 1 --logic prop /hi-bench/main-bench/TACAS17_ex/ex1_uf.c</p>
<p>why it is quick in prop? it is supposed to be very expensive!!</p>
hifrog - Bug #5010 (In Progress): Theoref bug: GNU MP: Cannot reallocate memory
https://scm.ti-edu.ch/issues/5010
2017-04-16T17:22:07Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>./hifrog --theoref mem.c —claim 143</p>
<p>GNU MP: Cannot reallocate memory (old_size=1184 new_size=1200)<br />Aborted (core dumped)</p>
hifrog - Bug #4998 (Feedback): bug in QF_BOOL: wrong result for prop in benchs in directrory ntdr...
https://scm.ti-edu.ch/issues/4998
2017-04-12T15:03:35Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>/hifrog --claim 1 --logic prop --bitwidth 8 --unwind 1 ~/hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c</p>
<p>VERIFICATION FAILED</p>
<p>wrong result! because claim 1 should hold</p>
hifrog - Bug #4997 (New): --theoref bug : quadratic explosion in ntdrivers-simplified benchmarks
https://scm.ti-edu.ch/issues/4997
2017-04-12T12:34:01Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>/hifrog --claim 1 --theoref ~/dev/hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c</p>
<p>Parts of debug:<br />...<br />....<br />; Warning: disabling SATElite preprocessing to track proof<br />^C^C<br />Program received signal SIGINT, Interrupt.<br />0x00000000005c300a in operator!= (a1=..., a2=...)<br /> at /home/asadis/dev/opensmt-debug/include/opensmt/Pterm.h:43<br />43 inline friend bool operator!= (const PTRef& a1, const PTRef& a2) { return a1.x != a2.x; }<br />(gdb) bt <br />#0 0x00000000005c300a in operator!= (a1=..., a2=...)<br /> at /home/asadis/dev/opensmt-debug/include/opensmt/Pterm.h:43<br />#1 0x00007ffff7acc7f4 in operator== (k1=..., k2=...) at ../../src/pterms/Pterm.h:69<br />#2 0x00007ffff7ad0e01 in Equal<PTLKey>::operator() (this=0x1d53ae9, k1=..., k2=...)<br /> at ../../src/minisat/mtl/Map.h:32<br />#3 0x00007ffff7ace677 in Map<PTLKey, PTRef, PTLHash, Equal<PTLKey> >::has (<br /> this=0x1d53ae8, k=...) at ../../src/minisat/mtl/Map.h:149<br />#4 0x00007ffff7accece in PtStore::hasBoolKey (this=0x1d539c0, k=...)<br /> at ../../src/pterms/PtStore.h:175<br />#5 0x00007ffff7ac5acf in Logic::insertTermHash (this=0x1d53708, sym=..., terms_in=...)<br /> at Logic.C:1111<br />#6 0x00007ffff7ac44e7 in Logic::mkEq (this=0x1d53708, args=...) at Logic.C:831<br />#7 0x00000000005ccaf2 in Logic::mkEq (this=0x1d53708, a1=..., a2=...)<br /> at /home/asadis/dev/opensmt-debug/include/opensmt/Logic.h:279<br />#8 0x00007ffff7aec8e8 in BVLogic::mkEq (this=0x1d53708, a1=..., a2=...) at BVLogic.h:274<br />#9 0x00007ffff7a7b942 in BitBlaster::notifyEquality (this=0x1e93410, tr=...)<br /> at BitBlaster.C:2202<br />#10 0x00007ffff7a7b449 in BitBlaster::notifyEqualities (this=0x1e93410)<br /> at BitBlaster.C:2162<br />#11 0x00000000005db719 in smtcheck_opensmt2t_cuf::refine_ce_mul (this=0x1e647e0, <br /> exprs=std::vector of length 2594, capacity 4096 = {...}, <br /> is=std::set with 1184 elements = {...}) at solvers/smtcheck_opensmt2_cuf.cpp:1442<br />#12 0x00000000005a58e1 in theory_refinert::assertion_holds_smt (this=0x7fffffffd2c0, <br /> assertion=..., store_summaries_with_assertion=true) at theory_refiner.cpp:178<br />#13 0x0000000000576027 in check_claims (ns=..., leaping_program=..., goto_functions=..., <br /> claim_map=std::map with 1 elements = {...}, <br /> claim_numbers=std::map with 2 elements = {...}, options=..., _message_handler=..., <br /> claim_nr=1) at check_claims.cpp:177<br />#14 0x0000000000570cf2 in funfrog_parseoptionst::check_function_summarization (<br /> this=0x7fffffffdd90, ns=..., goto_functions=...) at parseoptions.cpp:541<br />#15 0x0000000000570395 in funfrog_parseoptionst::doit (this=0x7fffffffdd90)<br />---Type <return> to continue, or q <return> to quit---q<br /> at parseoptionQuit<br />(gdb) f 9<br />....<br />...<br />main reason for this bug:<br />Theory combination between BV and CUF</p>
<p>need to be added millions of equalities in binding, indicating that qfcuf holds if and only if BV holds.</p>
OpenSMT 2 - Bug #3514 (Resolved): LRALogic.C:614: void LRALogic::splitTermToVarAndConst(const PTR...
https://scm.ti-edu.ch/issues/3514
2016-09-30T10:17:21Z
Karine Even Mendoza
karine.even_mendoza@kcl.ac.uk
<p>Code example: hi-bench/main-bench/funfrog_regression/03_simple/main7.c --show-error-trace --unwind 10</p>
Error:<br />Checking claims in program...<br />; Warning: disabling SATElite preprocessing to track proof<br />; Warning: disabling SATElite preprocessing to track proof<br /> Checking Claim #1 (100%) ...<br />Last assertion location: 30 / 36 ( 3)
<ul>
<li>INLINING function: c::__CPROVER_initialize</li>
<li>INLINING function: c::main<br />Processing a deferred function: c::__CPROVER_initialize<br />Processing a deferred function: c::main</li>
<li>INLINING function: c::strncpy<br />Processing a deferred function: c::strncpy<br />Unwinding loop c::strncpy.0 iteration 1 file main7.c line 7 function strncpy thread 0<br />Unwinding loop c::strncpy.0 iteration 2 file main7.c line 7 function strncpy thread 0<br />Unwinding loop c::strncpy.0 iteration 3 file main7.c line 7 function strncpy thread 0<br />Unwinding loop c::strncpy.0 iteration 4 file main7.c line 7 function strncpy thread 0<br />Unwinding loop c::strncpy.0 iteration 5 file main7.c line 7 function strncpy thread 0<br />Unwinding loop c::strncpy.0 iteration 6 file main7.c line 7 function strncpy thread 0<br />Unwinding loop c::strncpy.0 iteration 7 file main7.c line 7 function strncpy thread 0<br />Unwinding loop c::strncpy.0 iteration 8 file main7.c line 7 function strncpy thread 0<br />Unwinding loop c::strncpy.0 iteration 9 file main7.c line 7 function strncpy thread 0<br />Unwinding loop c::strncpy.0 iteration 10 file main7.c line 7 function strncpy thread 0<br />SYMEX TIME: 0.028<br />All SSA steps: 245<br />Ignored SSA steps after slice: 164<br />SLICER TIME: 0.001<br />evolcheck: LRALogic.C:614: void LRALogic::splitTermToVarAndConst(const PTRef&, PTRef&, PTRef&): Assertion `isRealTimes(term) || isRealDiv(term) || isRealVar(term) || isConstant(term)' failed.<br />Aborted (core dumped)</li>
</ul>
This is the code:
<ul>
<li>strncpy example */<br />//#include <stdio.h><br />//#include <string.h><br />#define LEN 2</li>
</ul>
<p>char *strncpy (char *dest, const char *src, int n) {<br /> for (int i = 0; i < n; ++i) {<br /> *dest = *src;<br /> if (!*src)<br /> return dest;<br /> ++dest;<br /> ++src;<br /> }<br /> return dest;<br />}</p>
<p>int main ()
{<br /> char str1[]= "To be ";<br /> char str2[LEN];<br /> strncpy (str2,str1,LEN-1);</p>
<pre><code>assert('T' == str1[0]);</code></pre>
<pre><code>//puts (str2);<br /> return 0;<br />}</code></pre>
<p>I don't think hifrog-lra can cop with it now, and so I expected to have an error from hifrog (or warning) not from opensmt2. Any idea what could be the reason?</p>
<p>Thanks,<br />Karine</p>
OpenSMT 2 - Bug #3502 (Resolved): Refinement benchmarks: get an exception - Logic::getOriginalAss...
https://scm.ti-edu.ch/issues/3502
2016-09-09T08:09:19Z
Karine Even Mendoza
karine.even_mendoza@kcl.ac.uk
<p>Code: hi-bench/main-bench/funfrog_regression/09_refinement/t_diff_e.c --refine-mode 2 --init-mode 1 --no-summary-optimization</p>
<p>Error: evolcheck: ../../src/logics/Logic.h:262: PTRef Logic::getOriginalAssertion(PTRef): Assertion `flat2orig.find(flat) != flat2orig.end()' failed.<br />Aborted (core dumped)</p>
<p>SMTlib code: in the attachment.</p>
OpenSMT 2 - Bug #3500 (Resolved): Hifrog - prop logic: Assertion `clause_in_A || clause_in_B' failed
https://scm.ti-edu.ch/issues/3500
2016-09-08T11:32:42Z
Karine Even Mendoza
karine.even_mendoza@kcl.ac.uk
<p>Happens when running all the claims at once. When running this benchmarks one claim after another (3 runs instead of 1), then there is no problem<br />Code example: /hi-bench/main-bench/funfrog_regression/05_McMillan/diskperf.cil_loopfree.c</p>
Output:<br />; ============================[ Search Statistics ]==============================<br />; | Conflicts | ORIGINAL | LEARNT | Progress |<br />; | | Vars Clauses Literals | Limit Clauses Lit/Cl | |<br />; ===============================================================================<br />; 0 | 0 0 | 53.660 s | 369.918 MB<br />SOLVER TIME: 54.877<br />UNSAT - it holds!<br />ASSERTION IS TRUE<br />Start generating interpolants...
<ol>
<li>Proof graph building begin</li>
<li>Memory used before building the proof: 371.594 MB</li>
<li>(1) Empty clause given in input or generated at preprocessing time: single node proof</li>
<li>Number of nodes: 1 (leaves: 0 - learnt: 0 - derived: 0 - theory: 0)</li>
<li>Maximum, average size of leaves: 0 -nan</li>
<li>Maximum, average size of learnt: 0 -nan</li>
<li>Number of edges: 0</li>
<li>Number of distinct variables in the proof: 0</li>
<li>Memory used after building the proof: 371.941 MB</li>
<li>Proof graph building end</li>
<li>Single interpolant </li>
<li>Using Pudlak for propositional interpolation<br />evolcheck: PGInterAux.C:210: opensmt::icolor_t ProofGraph::getClauseColor(const ipartitions_t&, const ipartitions_t&): Assertion `clause_in_A || clause_in_B' failed.<br />Aborted (core dumped)</li>
</ol>
OpenSMT 2 - Bug #3491 (Resolved): Segmentation fault in opensmt when using function summaries
https://scm.ti-edu.ch/issues/3491
2016-09-06T21:44:48Z
Karine Even Mendoza
karine.even_mendoza@kcl.ac.uk
<p>Code to reproduce the bug: hi-bench/main-bench/funfrog_regression/01_choice/main2_ok.c</p>
<p>When running the code for the first time we get unsat, on the second time we get seg. fault from opensmt.</p>
<p>There are several strange things going on:</p>
<p>1. When using the opensmt terminal the smt code runs ok (returns unsat for both executions). This is also the result when using Z3 website.<br />2. When using function summaries the most inner function is simply "true", but actually no code really removed (we just add another partition that is "true") - maybe something related to the way the partition is simplified?<br />3. The smt code when using summaries contains the original code, a partition that is true and a duplicated code (not sure it is related to the seg fault, but it can be a hint). It also says we are not using correctly the function summaries.</p>
<p>The original code (without function summaries):
==================================<br />(set-logic QF_LRA)<br />(declare-fun |funfrog::?callstart_symbol#3| () Bool)<br />(declare-fun |funfrog::?callend_symbol#3| () Bool)<br />(declare-fun |c::getchar::1::x!0#2| () Real)<br />(declare-fun |symex::nondet0| () Real)<br />(declare-fun |funfrog::c::getchar::?retval_tmp#1| () Real)<br />(declare-fun |funfrog::c::getchar::?retval#1| () Real)<br />(declare-fun |funfrog::?callstart_symbol#2| () Bool)<br />(declare-fun |funfrog::?callend_symbol#2| () Bool)<br />(declare-fun |funfrog::?error_symbol#1| () Bool)<br />(declare-fun |goto_symex::guard#1| () Bool)<br />(declare-fun |goto_symex::guard#2| () Bool)<br />(declare-fun |goto_symex::guard#3| () Bool)<br />(declare-fun |goto_symex::guard#4| () Bool)<br />(declare-fun |c::main::1::x!0#2| () Real)<br />(declare-fun |c::main::1::t!0#11| () Real)<br />(declare-fun .oite0 () Real)<br />(declare-fun |c::main::1::t!0#12| () Real)<br />(declare-fun .oite1 () Real)<br />(declare-fun |c::main::1::t!0#13| () Real)<br />(declare-fun .oite2 () Real)<br />(declare-fun |c::main::1::t!0#14| () Real)<br />(declare-fun .oite3 () Real)<br />(declare-fun |funfrog::?callstart_symbol#1| () Bool)<br />(declare-fun |funfrog::?callend_symbol#1| () Bool)<br />(assert<br /> (and<br />; XXX Partition: 0<br /> (and (= |c::getchar::1::x!0#2| |symex::nondet0|) (= |c::getchar::1::x!0#2| |funfrog::c::getchar::?retval_tmp#1|) (= |funfrog::c::getchar::?retval_tmp#1| |funfrog::c::getchar::?retval#1|) (or (not |funfrog::?callend_symbol#3|) (and (<= (- 1) |c::getchar::1::x!0#2|) (and |funfrog::?callstart_symbol#3| (<= (- 255) (* |c::getchar::1::x!0#2| (- 1)))))))<br />; XXX Partition: 1<br /> (and (= |funfrog::c::getchar::?retval#1| |c::main::1::x!0#2|) (= |goto_symex::guard#1| (= 1 |c::main::1::x!0#2|)) (= |goto_symex::guard#2| (= |c::main::1::x!0#2| 2)) (= |goto_symex::guard#3| (= |c::main::1::x!0#2| 3)) (= |goto_symex::guard#4| (= |c::main::1::x!0#2| (- 2))) (= |c::main::1::t!0#11| .oite0) (= |c::main::1::t!0#12| .oite1) (= |c::main::1::t!0#13| .oite2) (= |c::main::1::t!0#14| .oite3) (= |funfrog::?callstart_symbol#2| |funfrog::?callstart_symbol#3|) (= (not (or (not (and |funfrog::?callend_symbol#3| |funfrog::?callstart_symbol#2|)) (not (= (- 2) |c::main::1::t!0#14|)))) |funfrog::?error_symbol#1|) (or (not |funfrog::?callend_symbol#2|) (and |funfrog::?callend_symbol#3| |funfrog::?callstart_symbol#2|)))<br />; XXX Partition: 2<br /> (or |funfrog::?callstart_symbol#1| (not |funfrog::?callend_symbol#1|))<br />; XXX Partition: 3<br /> (and |funfrog::?error_symbol#1| |funfrog::?callstart_symbol#1| (= |funfrog::?callend_symbol#1| |funfrog::?callstart_symbol#2|))<br />; XXX oite symbol: .oite0<br />(and (or (not |goto_symex::guard#4|) (= (- 2) .oite0)) (or |goto_symex::guard#4| (= 10 .oite0)))<br />; XXX oite symbol: .oite1<br />(and (or (not |goto_symex::guard#3|) (= 5 .oite1)) (or |goto_symex::guard#3| (= |c::main::1::t!0#11| .oite1)))<br />; XXX oite symbol: .oite2<br />(and (or (not |goto_symex::guard#2|) (= 3 .oite2)) (or |goto_symex::guard#2| (= |c::main::1::t!0#12| .oite2)))<br />; XXX oite symbol: .oite3<br />(and (or (not |goto_symex::guard#1|) (= 1 .oite3)) (or |goto_symex::guard#1| (= |c::main::1::t!0#13| .oite3)))<br />))<br />(check-sat)</p>
<p>The code when using function summaries:
===============================<br />(set-logic QF_LRA)<br />(declare-fun |funfrog::?callstart_symbol#3| () Bool)<br />(declare-fun |funfrog::?callend_symbol#3| () Bool)<br />(declare-fun |funfrog::?callstart_symbol#2| () Bool)<br />(declare-fun |funfrog::?callend_symbol#2| () Bool)<br />(declare-fun |funfrog::?error_symbol#1| () Bool)<br />(declare-fun |goto_symex::guard#1| () Bool)<br />(declare-fun |goto_symex::guard#2| () Bool)<br />(declare-fun |goto_symex::guard#3| () Bool)<br />(declare-fun |goto_symex::guard#4| () Bool)<br />(declare-fun |c::main::1::x!0#2| () Real)<br />(declare-fun |funfrog::c::getchar::?retval#1| () Real)<br />(declare-fun |c::main::1::t!0#11| () Real)<br />(declare-fun .oite0 () Real)<br />(declare-fun |c::main::1::t!0#12| () Real)<br />(declare-fun .oite1 () Real)<br />(declare-fun |c::main::1::t!0#13| () Real)<br />(declare-fun .oite2 () Real)<br />(declare-fun |c::main::1::t!0#14| () Real)<br />(declare-fun .oite3 () Real)<br />(declare-fun |funfrog::?callend_symbol#1| () Bool)<br />(declare-fun |c::getchar::1::x!0#2| () Real)<br />(declare-fun |symex::nondet0| () Real)<br />(declare-fun |funfrog::c::getchar::?retval_tmp#1| () Real)<br />(declare-fun .oite4 () Real)<br />(declare-fun .oite5 () Real)<br />(declare-fun .oite6 () Real)<br />(declare-fun .oite7 () Real)<br />(assert<br /> (and<br />; XXX Partition: 0<br /> true<br />; XXX Partition: 1<br /> (and (= |c::main::1::x!0#2| |funfrog::c::getchar::?retval#1|) (= |goto_symex::guard#1| (= 1 |c::main::1::x!0#2|)) (= |goto_symex::guard#2| (= |c::main::1::x!0#2| 2)) (= |goto_symex::guard#3| (= |c::main::1::x!0#2| 3)) (= |goto_symex::guard#4| (= |c::main::1::x!0#2| (- 2))) (= |c::main::1::t!0#11| .oite0) (= |c::main::1::t!0#12| .oite1) (= |c::main::1::t!0#13| .oite2) (= |c::main::1::t!0#14| .oite3) (= |funfrog::?callstart_symbol#2| |funfrog::?callstart_symbol#3|) (= (not (or (not (and |funfrog::?callend_symbol#3| |funfrog::?callstart_symbol#2|)) (not (= (- 2) |c::main::1::t!0#14|)))) |funfrog::?error_symbol#1|) (or (not |funfrog::?callend_symbol#2|) (and |funfrog::?callend_symbol#3| |funfrog::?callstart_symbol#2|)))<br />; XXX Partition: 2<br /> (and |funfrog::?error_symbol#1| (= |funfrog::?callend_symbol#1| |funfrog::?callstart_symbol#2|))<br />; XXX Partition: 3<br /> (and (= |c::getchar::1::x!0#2| |symex::nondet0|) (= |c::getchar::1::x!0#2| |funfrog::c::getchar::?retval_tmp#1|) (= |funfrog::c::getchar::?retval#1| |funfrog::c::getchar::?retval_tmp#1|) (or (not |funfrog::?callend_symbol#3|) (and (<= (- 1) |c::getchar::1::x!0#2|) (and |funfrog::?callstart_symbol#3| (<= (- 255) (* (- 1) |c::getchar::1::x!0#2|))))))<br />; XXX Partition: 4<br /> (and (= |c::main::1::x!0#2| |funfrog::c::getchar::?retval#1|) (= |goto_symex::guard#1| (= 1 |c::main::1::x!0#2|)) (= |goto_symex::guard#2| (= |c::main::1::x!0#2| 2)) (= |goto_symex::guard#3| (= |c::main::1::x!0#2| 3)) (= |goto_symex::guard#4| (= |c::main::1::x!0#2| (- 2))) (= |funfrog::?callstart_symbol#2| |funfrog::?callstart_symbol#3|) (= (not (or (not (and |funfrog::?callend_symbol#3| |funfrog::?callstart_symbol#2|)) (not (= (- 2) |c::main::1::t!0#14|)))) |funfrog::?error_symbol#1|) (or (not |funfrog::?callend_symbol#2|) (and |funfrog::?callend_symbol#3| |funfrog::?callstart_symbol#2|)) (= |c::main::1::t!0#11| .oite4) (= |c::main::1::t!0#12| .oite5) (= |c::main::1::t!0#13| .oite6) (= |c::main::1::t!0#14| .oite7))<br />; XXX Partition: 5<br /> (and |funfrog::?error_symbol#1| (= |funfrog::?callend_symbol#1| |funfrog::?callstart_symbol#2|))<br />; XXX oite symbol: .oite0<br />(and (or (not |goto_symex::guard#4|) (= (- 2) .oite0)) (or |goto_symex::guard#4| (= 10 .oite0)))<br />; XXX oite symbol: .oite1<br />(and (or (not |goto_symex::guard#3|) (= 5 .oite1)) (or |goto_symex::guard#3| (= |c::main::1::t!0#11| .oite1)))<br />; XXX oite symbol: .oite2<br />(and (or (not |goto_symex::guard#2|) (= 3 .oite2)) (or |goto_symex::guard#2| (= |c::main::1::t!0#12| .oite2)))<br />; XXX oite symbol: .oite3<br />(and (or (not |goto_symex::guard#1|) (= 1 .oite3)) (or |goto_symex::guard#1| (= |c::main::1::t!0#13| .oite3)))<br />; XXX oite symbol: .oite4<br />(and (or (not |goto_symex::guard#4|) (= (- 2) .oite4)) (or |goto_symex::guard#4| (= 10 .oite4)))<br />; XXX oite symbol: .oite5<br />(and (or (not |goto_symex::guard#3|) (= 5 .oite5)) (or |goto_symex::guard#3| (= |c::main::1::t!0#11| .oite5)))<br />; XXX oite symbol: .oite6<br />(and (or (not |goto_symex::guard#2|) (= 3 .oite6)) (or |goto_symex::guard#2| (= |c::main::1::t!0#12| .oite6)))<br />; XXX oite symbol: .oite7<br />(and (or (not |goto_symex::guard#1|) (= 1 .oite7)) (or |goto_symex::guard#1| (= |c::main::1::t!0#13| .oite7)))<br />))<br />(check-sat)</p>
<p>I also trace a similar problem in: (maybe use it, it the code is easier to debug/smaller?)<br />hi-bench/main-bench/funfrog_regression/03_simple/main4.c<br />hi-bench/main-bench/funfrog_regression/06_globals/main2.c<br />hi-bench/main-bench/funfrog_regression/06_globals/main3.c<br />hi-bench/main-bench/funfrog_regression/06_globals/main4.c</p>
<p>If one of these is better for testing, I'll add the smt code of it (please let me know if needed)</p>
OpenSMT 2 - Bug #3488 (Resolved): SIGSEGV in LRASolver
https://scm.ti-edu.ch/issues/3488
2016-09-06T07:48:15Z
Antti Hyvärinen
Antti.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>
pre-commit-hooks - Feature #3267 (New): Replace Files
https://scm.ti-edu.ch/issues/3267
2016-06-03T09:49:09Z
Erich Foster
erich.foster@usi.ch
<p>Stop asking to replace hooks which are the same.</p>
cow - Bug #863 (Resolved): Missing Mesh File for Wall2
https://scm.ti-edu.ch/issues/863
2015-07-06T13:06:13Z
Erich Foster
erich.foster@usi.ch
<p>In the master branch the mesh file for wall2 is missing, i.e. examples/wall2/ventricle_X_axis2.e</p>
cow - Bug #862 (New): Cow doesn't compile for Moose Build 43 (PULL REQUEST)
https://scm.ti-edu.ch/issues/862
2015-07-06T13:00:51Z
Erich Foster
erich.foster@usi.ch
<p>The master branch still doesn't compile for the latest version of Moose. The problem is _f in include/materials/GuccioneCostaRot.h this should be a constant.</p>