Project

General

Profile

To do #7717

Implement theory propagation also for PRODUCE_PROOF version

Added by Martin Blicha about 1 year ago.

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.

Also available in: Atom PDF