> 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? Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev