Re: [isabelle] SAT solver problem
> I have problem with using nitpick even for trivial lemma such as: lemma "P
> â Q ".
> in the output panel, I've got this kodkod warning:
> Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
> I'm using Isabelle 2016 64-bit windows version. Any suggestion?
This seems to be a low-level issue. There are hard to debug; let's see if there's a workaround first.
In the Nitpick documentation (isabelle doc nitpick), there's a list of SAT solvers that can be tried. You can choose one by setting
nitpick_params [sat_solver = <name_of_solver>]
Could you try e.g. MiniSat as the solver and see if the issue goes away?
This archive was generated by a fusion of
Pipermail (Mailman edition) and