In Z3Solver, check for nary encoding errors
Add CVC4 solver