Martin Blicha
- Email: blicha@d3s.mff.cuni.cz
- Registered on: 17/01/2017
- Last connection: 12/10/2023
Issues
Projects
- OpenSMT 2 (Manager, Developer, 11/10/2017)
- hifrog (Manager, Developer, 18/01/2017)
- hi-bench (Manager, Developer, 05/04/2017)
- smts (Developer, 18/01/2019)
- verify solidity contracts (Manager, 24/10/2022)
- verify witness evaluation (Manager, Developer, 27/11/2020)
Activity
11/04/2019
- 11:18 OpenSMT 2 Bug #10647 (New): UF benchmark crash
07/09/2018
29/08/2018
- 15:29 hifrog Bug #7795: Type constraints option for LA theories
- The example is missing function declaration.
unsigned int nondetUInt();
With that, the assertions are verified ...
24/08/2018
- 16:05 hifrog Bug #7760 (New): Infinite loop in theory refinement
- In current version (e.g. f4aaed49) there is bug in theory refinement algorithm. In cases 6 and 7 there is an infinite...
21/08/2018
- 13:39 hifrog To do #7602 (Closed): Remove dependency on boost
- Unit tests have been added and can be extended if any issue regarding this is found.
- 13:36 hifrog To do #7728 (New): Refactor theory refinement code
- Code related to theory refinement should be refactored/simplfied.
Karine should have some version prepared.
16/08/2018
- 15:00 OpenSMT 2 To do #7717 (New): Implement theory propagation also for PRODUCE_PROOF version
- Theory propagation is now disabled for PRODUCE_PROOF version (see beginning of CoreSMTSolver::search method).
The re... - 14:57 OpenSMT 2 To do #4536 (Closed): Progettazione e combinazione attraverso algoritmo
- 14:56 OpenSMT 2 To do #4537 (Closed): Requisiti
- 14:56 OpenSMT 2 To do #4538 (Closed): database
Also available in: Atom