General

Profile

Martin Blicha

Issues

Projects

Activity

07/09/2018

21:50 hifrog To do #7600 (Resolved): Cleaning check_sum_theoref_single

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