USI & SUPSI Source Code Management (SCM): Issues
https://scm.ti-edu.ch/
https://scm.ti-edu.ch/favicon.ico?1560171137
2019-10-06T22:15:21Z
USI & SUPSI Source Code Management (SCM)
Redmine
hifrog - Bug #13577 (New): prop incorrect result
https://scm.ti-edu.ch/issues/13577
2019-10-06T22:15:21Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>Benchmark: ex21-upg2.c (attached)</p>
<p>How to run:<br />./hifrog --logic prop ex21-upg2.</p>
<p>Error:<br />reported as Successful but I think a= 1 and b=1 is a CEX. Surprisingly CBMC also agrees as Successful!</p>
hifrog - Bug #13356 (Resolved): Bug in Hifrog LRA encoding - resulting assertion violation for a ...
https://scm.ti-edu.ch/issues/13356
2019-09-26T11:54:36Z
Sepideh Asadi
sepideh.a65@gmail.com
<p><strong>Benchmark</strong>: ex13-change-orig.c (attached)</p>
<p><strong>How to run:</strong><br />./hifrog --logic qflra ex13-change-orig.c</p>
<p><strong>Error:</strong><br />LRA reports the bench as unsafe, while prop reports it as safe. The result of dump-query is SAT in OpenSMT and Z3, so the bug is in the encoding.</p>
OpenSMT 2 - Bug #10647 (New): UF benchmark crash
https://scm.ti-edu.ch/issues/10647
2019-04-11T09:18:00Z
Martin Blicha
blicha@d3s.mff.cuni.cz
hifrog - To do #10434 (New): Automatically detect the bound in HiFrog for the sake of completeness
https://scm.ti-edu.ch/issues/10434
2019-03-29T13:52:40Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>Developing a preprocessing mechanism to detect the necessary depth of unrolling the program.(completeness threshold)<br />Then we can claim on verification of those instances, not just falsification.</p>
hifrog - To do #9433 (New): strong itp-lra-algorithm generates redundant formula
https://scm.ti-edu.ch/issues/9433
2018-11-28T21:43:13Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>investigate LRA strong itp Alg and compare the result with weak one; it seems weak mode generates compact and good summary, the same as TACAS version, but STRONG mode contains some redundant parts in the formula.</p>
<p>------------------------------------------<br />example:<br />short get_nondet_short();</p>
<p>int abs(int x) {<br /> return x >= 0 ? x : -x;<br />}</p>
<p>int main() {<br /> int x = get_nondet_short();<br /> x = abs(x);<br /> int y = x + 2;<br /> assert(y >= 0);<br />}</p>
<p>------------------------------------------<br />How to run?</p>
<p>weak: <br />./hifrog --logic qflra --itp-lra-algorithm 2 example.c</p>
<p>strong:<br />./hifrog --logic qflra --itp-lra-algorithm 0 example.c</p>
hifrog - To do #7864 (New): investigate the functionality of --no-assert-grouping
https://scm.ti-edu.ch/issues/7864
2018-09-08T18:23:22Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>2-Enable this functionality:<br />--no-assert-grouping : do not group checks for the same assertion with the different call stack.</p>
<p>This option when is enabled will increase the possibility of holding the assertion for a specific function.</p>
hifrog - To do #7863 (New): report system in HiFrog
https://scm.ti-edu.ch/issues/7863
2018-09-08T18:19:17Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>Design a separate class as a report class in HiFrog (storing in the Buffer beforehand) - (due to performance)</p>
hifrog - To do #7862 (New): enable summary re-use in CUF
https://scm.ti-edu.ch/issues/7862
2018-09-08T18:08:22Z
Sepideh Asadi
sepideh.a65@gmail.com
<p>CUF generates summary but does not reload(re-use) it.</p>
OpenSMT 2 - To do #7717 (New): Implement theory propagation also for PRODUCE_PROOF version
https://scm.ti-edu.ch/issues/7717
2018-08-16T13:00:25Z
Martin Blicha
blicha@d3s.mff.cuni.cz
<p>Theory propagation is now disabled for PRODUCE_PROOF version (see beginning of CoreSMTSolver::search method).<br />The reason is that literals derived by theory propagation do not have reason set at the moment, but this is expected by the proof logging.</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>