diff --git a/src/plugins/wp/tests/wp_plugin/float_format.i b/src/plugins/wp/tests/wp_plugin/float_format.i index cee1e6f724b18f850abf81ed2ca31b4f373a7236..cdca1c6d758b266bfcef3b4a3727f19a234f8500 100644 --- a/src/plugins/wp/tests/wp_plugin/float_format.i +++ b/src/plugins/wp/tests/wp_plugin/float_format.i @@ -1,7 +1,7 @@ /* run.config_qualif OPT: -wp-prover native:coq - OPT: -wp-prover native:alt-ergo -wp-steps 50 -wp-timeout 1 - OPT: -wp-prover alt-ergo -wp-steps 50 -wp-timeout 1 + OPT: -wp-prover native:alt-ergo -wp-steps 5 -wp-timeout 100 + OPT: -wp-prover alt-ergo -wp-steps 5 -wp-timeout 100 */ //@ ensures KO: \result == 0.2 + x ; diff --git a/src/plugins/wp/tests/wp_plugin/math.i b/src/plugins/wp/tests/wp_plugin/math.i index 3fece066d5a57e4ab2eb985cd98223ce0b839618..160d94e7bee83c4caeeff4227a9a579d10c923a9 100644 --- a/src/plugins/wp/tests/wp_plugin/math.i +++ b/src/plugins/wp/tests/wp_plugin/math.i @@ -5,8 +5,8 @@ /* run.config_qualif OPT: -wp-prover alt-ergo -wp-prop=-ko -wp-timeout 100 -wp-steps 1500 OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=-ko -wp-timeout 100 -wp-steps 1500 - OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 1 -wp-steps 50 - OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=ko -wp-timeout 1 + OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 100 -wp-steps 10 + OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=ko -wp-timeout 100 -wp-steps 10 */ // -------------------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle index 2c38f9528386738d0a567c89fe077120d64ea292..fd00d9ebd5b3572c8a1acd500ba6df167dcf7384 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 1 -wp-steps 50 [...] +# frama-c -wp -wp-timeout 100 -wp-steps 5 [...] [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle index 0d212aebf6a888e2d9da199a9eaa90b1bb04fecf..5974584a73c3314ee7219f84e732d7bbe21260be 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 1 -wp-steps 50 [...] +# frama-c -wp -wp-timeout 100 -wp-steps 5 [...] [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing) [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3. diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle index b3a0b092a29b49e93370bbb7eef46793cc412c55..6dd9859b66923ba3291bb6433d7017c18ef0d153 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 1 -wp-steps 50 [...] +# frama-c -wp -wp-timeout 100 -wp-steps 10 [...] [kernel] Parsing tests/wp_plugin/math.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle index f3f9a9692dfaf4ff5f641fc02d4efb1050a523d5..5b07b133292e5f331f03ec150346b916870de08f 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-timeout 1 [...] +# frama-c -wp -wp-timeout 100 -wp-steps 10 [...] [kernel] Parsing tests/wp_plugin/math.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver'