Hello Sandrine, > I am using why3 version 1.3.3 and would like to add the Z3 and E provers > to the list of installed provers, so that they are triggered by proof > strategies 0, 1 and more. I tried several versions (among those listed > in provers-detection-data.conf), including Z3 version 4.8.4 (that is > mentioned in the documentation for proof strategies). However, none of > them is triggered by strategies 0 and 1. Which version of Z3 and E > should I use?
Your Why3 configuration file should contain the code of the strategies. It looks like ---------------------------------------- [strategy] code = "c Alt-Ergo 1 1000 c CVC4,1.7 1 1000 c Z3,4.8.4 1 1000 " desc = "Automatic@ run@ of@ main@ provers" name = "Auto_level_0" shortcut = "0" ---------------------------------------- The versions of the provers are included in this code (except for "Alt-Ergo" here, which is defined as an alias for a specific version of Alt-Ergo somewhere else in the configuration file). Best regards, -- Jean-Christophe _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
