CVC4-SymBreak: Derived SMT solver at SMT Competition 2019

08/02/2019
by   Saket Dingliwal, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset