La codificación devuelve "desconocido"
Para este ejemplo:http://pastebin.com/QyebfD1p z3 y cvc4 devuelven "desconocido" como resultado de check-sat. Ambos no son muy detallados sobre la causa, ¿hay alguna manera de hacer que z3 sea más detallado acerca de su ejecución?