The naive solver now handles assumptions
Added options to Kind2 solver