Hello, I did not use CVC4 1.5 for enough time to compare with 1.4. Anyway, I'd like to recommend:
1) to duplicate the prover entry, with an alternative name, instead of modifying the existing one 2) to use the *-step options of CVC4 only for the "command_steps" parameter, not the "command" one. In other words, do not modify but add a new entry in why3.conf e.g. such as [prover] alternative ="Variant" command = "cvc4 --lang=smt2 --stats --no-cbqi --nl-ext --no-cond-rewrite-quant --inst-no-entail %f" command_steps = "cvc4 --lang=smt2 --stats --no-cbqi --nl-ext --no-cond-rewrite-quant --inst-no-entail --bitblast-step=5 --cnf-step=5 --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 --rewrite-step=0 --rlimit=%S %f" driver = "cvc4.drv" name = "CVC4" shortcut = "cvc4" version = "1.5" This will allow you to use both variants in each VC, and indeed compare them. Please do not hesitate to inform us through this list if the modified parameters make CVC4 significantly more efficient on your examples. - Claude Le 07/08/2017 à 22:36, Yannick Moy a écrit : > Hi Jens, > >> I am, however, unsure about the proper way to pass these options to >> CVC4 (1.5) through the ‘.why3.conf’ file. >> Could you please point out how I should modify the why3 configuration >> file? > > Here is what you could put in your version of why3.conf: > > [prover] > command = "cvc4 --lang=smt2 --stats --no-cbqi --nl-ext > --no-cond-rewrite-quant --inst-no-entail --bitblast-step=5 --cnf-step=5 > --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 > --rewrite-step=0 %f" > command_steps = "cvc4 --lang=smt2 --stats --no-cbqi --nl-ext > --no-cond-rewrite-quant --inst-no-entail --bitblast-step=5 --cnf-step=5 > --lemma-step=5 --parse-step=0 --preprocess-step=0 --restart-step=10 > --rewrite-step=0 --rlimit=%S %f" > driver = "cvc4.drv" > name = "CVC4" > shortcut = "cvc4" > version = "1.5" > > (what really matters here is the "command" field, you may not need the > "command_steps" field in your case) > -- > 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
