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 = "/home/cmarche/.opam/4.04.0/lib/why3/plugins/tptp" ... And, of course, if the plugin path is there, check whether the dynamic library is there, e.g. if the file /home/cmarche/.opam/4.04.0/lib/why3/plugins/tptp.cmxs is present - Claude Le 14/11/2017 à 12:31, Yannick Moy a écrit : > 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. > But it just answers with: > > $ why3 prove -P Eprover quantarrays.mlw > Unknown printer 'tptp-fof' > > Do you get this error when calling TPTP provers? > Should I configure why3 differently? > > Thanks in advance. > -- > Yannick Moy, Senior Software Engineer, AdaCore > > > > > > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
