The problem seems ot be the --strings-exp option. If I remove that, cvc4 seems to work fine.
julia diff --git a/share/provers-detection-data.conf b/share/provers-detection-data.conf index a85e609e4..eac39d396 100644 --- a/share/provers-detection-data.conf +++ b/share/provers-detection-data.conf @@ -75,8 +75,8 @@ version_ok = "1.7" driver = "cvc4_17" # --random-seed=42 is not needed as soon as --random-freq=0.0 by default # to try: --inst-when=full-last-call -command = "%e --stats --tlimit=%t000 --lang=smt2 --strings-exp %f" -command_steps = "%e --stats --rlimit=%S --lang=smt2 --strings-exp %f" +command = "%e --stats --tlimit=%t000 --lang=smt2 %f" +command_steps = "%e --stats --rlimit=%S --lang=smt2 %f" use_at_auto_level = 1 # CVC4 version 1.6 _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
