RUN: $(CloneModelSampleSat)