TxPathCondition::unsatCoreInterpolation has to be made more efficient, perhaps by making the combining of simplification core and unsat core in TimingSolver::evaluate and elsewhere ordered, so that linear scan of constraints O(n) with n the path length would work instead of O(n log n). Where at each constraint, we test if the constraint was in the core or not.
TxPathCondition::unsatCoreInterpolationhas to be made more efficient, perhaps by making the combining of simplification core and unsat core inTimingSolver::evaluateand elsewhere ordered, so that linear scan of constraints O(n) with n the path length would work instead of O(n log n). Where at each constraint, we test if the constraint was in the core or not.EDIT: Changed TxTreeNode to TxPathCondition