5

TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on the other hand, is a method of analyzing programs. Symbolic execution usually relies on SAT and SMT solvers, but not the other way around. SAT and SMT solvers ...


3

Some SAT solvers and SMT solvers offer an interface that lets you push clauses, and then later pop/retract them and push some new ones. You could explore to see whether this offers a speedup in your situation. There are no guarantees, and the only way to tell is to try it.


1

I don't see any gap in your understanding. What you wrote looks correct to me. Perhaps the author meant to use the property $P := c \le n+1 \land n \ge 1$. I think with that modification, $P$ becomes 1-inductive but not 0-inductive. I suspect the author was looking for a simple example of a property that is 1-inductive but not 0-inductive, and missed a ...


Only top voted, non community-wiki answers of a minimum length are eligible