diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle index 0d2d5f9b4b0378b0c566fbcd074616353cb6a655..ab4451e7b05126a076003f9d0c98f00efca996ef 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Real)' [...] [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle index df0b9d2b62309b6f2078ffb86d76b448cf8e5d35..d2cccc3d319aaf4d8f39e61cdaf04a28d717b99b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle @@ -1,4 +1,4 @@ -# frama-c -wp -wp-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...] +# frama-c -wp -wp-model 'Typed (Real)' [...] [kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing) [wp] Running WP plugin... [wp] Loading driver 'share/wp.driver' diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/0229e4d03dbe5dab56c7710d10ede856.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/0229e4d03dbe5dab56c7710d10ede856.json new file mode 100644 index 0000000000000000000000000000000000000000..b875f72878672c071518369a3e24ffe8ff01f98b --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/0229e4d03dbe5dab56c7710d10ede856.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0057, + "steps": 4 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/5a2626cdfff12f90f4c43a8b11ff70fb.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/5a2626cdfff12f90f4c43a8b11ff70fb.json new file mode 100644 index 0000000000000000000000000000000000000000..cdba4fe113543f699c812db47d6cbe7d2fa2ba20 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/5a2626cdfff12f90f4c43a8b11ff70fb.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0047, + "steps": 4 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/d189bb3b47019848c9af5b14c2febb1c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/d189bb3b47019848c9af5b14c2febb1c.json new file mode 100644 index 0000000000000000000000000000000000000000..16eacff0af61e1b60c56f922f046783dfb7dc0ff --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/d189bb3b47019848c9af5b14c2febb1c.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0056, + "steps": 4 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/e2c00d7a3ff17960fa10dee8b619ee99.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/e2c00d7a3ff17960fa10dee8b619ee99.json new file mode 100644 index 0000000000000000000000000000000000000000..4d58671fa0e00cc8296590f2ad4014d8c431e7f9 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/e2c00d7a3ff17960fa10dee8b619ee99.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.005, + "steps": 4 }