[isabelle-dev] cvc4

[Jasmin Blanchette]

> On 5 Aug 2017, at 09:16, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> A new version has appeared and now sledgehammer always complains about “abnormal termination”.

Could you send me the following details?

1. Platform (e.g. macOS 10.12.2)
2. The output of "isabelle getenv CVC4_SOLVER"
3. A concrete example to reproduce the problem

Also, could you try adding the line

	declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant"]]

somewhere in your theory file and try CVC4 again?

Jasmin