- Email: firstname.lastname@example.org
- Registered on: 16/03/2016
- Last connection: 24/10/2019
- 00:15 hifrog Bug #13577 (New): prop incorrect result
- Benchmark: ex21-upg2.c (attached)
How to run:
./hifrog --logic prop ex21-upg2.
reported as Successful...
- 00:11 hifrog Bug #13356 (Resolved): Bug in Hifrog LRA encoding - resulting assertion violation for a safe bench
- This behaviour is Normal and expected in LRA, because LRA does not recognise int, all is Real number!
it is becaus...
- 13:54 hifrog Bug #13356 (Resolved): Bug in Hifrog LRA encoding - resulting assertion violation for a safe bench
- *Benchmark*: ex13-change-orig.c (attached)
*How to run:*
./hifrog --logic qflra ex13-change-orig.c
- 14:52 hifrog To do #10434 (New): Automatically detect the bound in HiFrog for the sake of completeness
- Developing a preprocessing mechanism to detect the necessary depth of unrolling the program.(completeness threshold)
- 22:43 hifrog To do #9433 (New): strong itp-lra-algorithm generates redundant formula
- investigate LRA strong itp Alg and compare the result with weak one; it seems weak mode generates compact and good su...
- 20:23 hifrog To do #7864 (New): investigate the functionality of --no-assert-grouping
- 2-Enable this functionality:
--no-assert-grouping : do not group checks for the same assertion with the dif...
- 20:19 hifrog To do #7863 (New): report system in HiFrog
- Design a separate class as a report class in HiFrog (storing in the Buffer beforehand) - (due to performance)
- 20:08 hifrog To do #7862 (New): enable summary re-use in CUF
- CUF generates summary but does not reload(re-use) it.
- 22:19 hifrog To do #7861 (New): A minimal necessary unwinding bound
- A minimal necessary unwinding bound
A lazy enumeration of unrollings, it is something that CBMC is doing in SVCOMP.
- 22:15 hifrog To do #7860 (New): follow up in EUF summaries (Grisha's idea)
- The point is about the loop in function func which calculates a new value for variable b. This loop is not needed for...
Also available in: Atom