Hi, Hossein Sheini (University of Michigan) translated several Wisconsin Safety Analyzer (WiSA) benchmarks to the SMT-LIB format. These benchmarks are in the QF_UFLIA (uninterpreted functions + linear integer arithmetic) division. The benchmarks can be downloaded at: http://www.csl.sri.com/users/demoura/smt-comp/benchmarks.shtml Leonardo