This is a demo of how to use java-smt based on the template and tutorial from sosy-lab/java-smt. We use a pure Java-based SMT solver. For more SMT solvers, e.g., Z3 binaries, please refer to the above tutorial.
We demonstrate the use of JavaSMT by solving two tasks from the lecture and exercises of the Formal Methods for Software Engineering module.
First, we show how to encode and solve a simple emoji math puzzle in class EmojiSolver. This example only uses integer arithmetic.
Second, we show how to encode a PC configuration problem in class PCConfigSolver. This example combines propositional logic and simple integer arithmetic.
A video is available from https://youtu.be/9ptEo4apVcU.