RUN: $(StepFunctionSampleSat)