Martin Blicha
Activity
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
- 14:56 OpenSMT 2 To do #4539 (Closed): pagamento
Also available in: Atom