SMT solving
Model replay
Evaluating a returned model against the original query.
Definition
Model replay
Model replay checks a sat result by substituting returned values into the original parsed terms and evaluating every assertion.
Replay can catch errors in lowering, search, or model construction when the original evaluator is independent of those steps. It gives direct evidence for the reported assignment.
01
Example
If a solver returns x = 6 and y = 4 for x + y = 10 and x > y, replay evaluates both assertions as true.
02
Important distinction
Replay supports sat. It cannot prove unsat because there is no model to evaluate.
After reading this article, you should be able to
- Define Model replay in the sense used on this site.
- Explain which solver errors model replay can detect and which result it cannot certify.