An SMT (1-2-1) encoding of a Simple C FooBar Function Try the foorbar function smt-encoding using online SMT solver CVC4. The solver finds input values that violate an assertion in the program.