-- Yannick Moy (2017-11-14)
> indeed, why3config did not generate the "plugin" line.
> But in any case, I have no such "/lib/why3/plugins/tptp" in my source or
> installed why3 directory.
> How do I get this created? Is it a special argument to configure?
Forget that, my setup is broken. I'll
-- Claude Marché (2017-11-14)
> The TPTP printer is in a dynamically loaded plugin, so you should check
> your why3.conf file, that needs to contain the appropriate plugin path,
> e.g.:
indeed, why3config did not generate the "plugin" line.
But in any case, I have no such "/lib/why3/plugins/tptp"
The TPTP printer is in a dynamically loaded plugin, so you should check
your why3.conf file, that needs to contain the appropriate plugin path,
e.g.:
[main]
loadpath = "/home/cmarche/.opam/4.04.0/share/why3/theories"
loadpath = "/home/cmarche/.opam/4.04.0/share/why3/modules"
plugin =
Hi Why3 crowd,
I tried to use a resolution based prover, to see if it could solve some VCs
that SMT solvers have a hard time with, typically when there is no trigger to
instantiate some conflicting axioms.
So I installed Eprover, and I called it from why3 that I built from up-to-date
sources.
