The SAT solver CDCL still produces model values for symbols that have been popped of the context. For instance this input file:
(set-option :produce-models true)
(set-logic ALL)
(declare-const x Int)
(push 1)
(declare-fun f (Int) Int)
(assert (= (f 0) 1))
(pop 1)
; The function `f` isn't declared anymore in the current context and we must
; not produce a model value for it.
(check-sat)
(get-model)
produces a value for f with CDCL but does not it with CDCL-Tableaux.
The SAT solver
CDCLstill produces model values for symbols that have been popped of the context. For instance this input file:produces a value for
fwithCDCLbut does not it withCDCL-Tableaux.