get-assignment sometimes returns unknown, and we even use such cases in regression tests, e.g. in test/regression/base/incremental/assignment_global.smt2.
The test does not output unknown if trackPartitions() evaluates to true (i.e., with produce-proofs).
It uses MainSolver::getTermValue, and it seems that term_mapper->hasLit(tr) is not working properly here - it claims that the xor term is not present in TermMapper, hence returning unknown.
get-assignmentsometimes returnsunknown, and we even use such cases in regression tests, e.g. intest/regression/base/incremental/assignment_global.smt2.The test does not output
unknowniftrackPartitions()evaluates to true (i.e., withproduce-proofs).It uses
MainSolver::getTermValue, and it seems thatterm_mapper->hasLit(tr)is not working properly here - it claims that the xor term is not present inTermMapper, hence returningunknown.