> On 5 Aug 2017, at 09:16, Lawrence Paulson <l...@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?


isabelle-dev mailing list

Reply via email to