Actions
To do #7717
openImplement theory propagation also for PRODUCE_PROOF version
Status:
New
Priority:
High
Assignee:
-
Start date:
16/08/2018
Due date:
% Done:
0%
Estimated time:
Description
Theory propagation is now disabled for PRODUCE_PROOF version (see beginning of CoreSMTSolver::search method).
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.
No data to display
Actions