CVC4-SymBreak: Derived SMT solver at SMT Competition 2019

08/02/2019

∙

by   Saket Dingliwal, et al.

∙

0

∙

share

We present CVC4-SymBreak, a derived SMT solver based on CVC4, and a non-competing participant of SMT-COMP 2019. Our technique exploits symmetries over the Boolean skeleton variables in an SMT problem to prune the search space. We use an ensemble of a solver with and without symmetries to be more effective. Our approach results in significantly faster solutions on a subset of available SMT benchmarks.