diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/5863bcb9783af8198ea3c259e56a7924.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/5863bcb9783af8198ea3c259e56a7924.json new file mode 100644 index 0000000000000000000000000000000000000000..8ab930568034361eb29799ade59eb8882e308d8f --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/5863bcb9783af8198ea3c259e56a7924.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0163, + "steps": 26 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/779eeed2fb0538630cac0ff491a5a29c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/779eeed2fb0538630cac0ff491a5a29c.json new file mode 100644 index 0000000000000000000000000000000000000000..8f61a59ddf50f8dc3b1a592be5bd4fcc87fd041f --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/779eeed2fb0538630cac0ff491a5a29c.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0164, + "steps": 9 } diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/d1df1e6aa6d901d0b6a6852170a14b29.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/d1df1e6aa6d901d0b6a6852170a14b29.json new file mode 100644 index 0000000000000000000000000000000000000000..b81312cd9592534507b54fc6cbfc9fd8300675f1 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.session/cache/d1df1e6aa6d901d0b6a6852170a14b29.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0102, + "steps": 12 } diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.0.session/cache/c74996e8ecbe3a35835609127c6e2b4e.json b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.0.session/cache/c74996e8ecbe3a35835609127c6e2b4e.json new file mode 100644 index 0000000000000000000000000000000000000000..e61b1e995698e8827e0c547e98748fc339fdd03f --- /dev/null +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.0.session/cache/c74996e8ecbe3a35835609127c6e2b4e.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0126, + "steps": 18 } diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/2ba962f82cf233aaa33bee4e5a4ef868.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/2ba962f82cf233aaa33bee4e5a4ef868.json new file mode 100644 index 0000000000000000000000000000000000000000..cb6217f3a67661b91e92bc31de70961fb5f37856 --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/2ba962f82cf233aaa33bee4e5a4ef868.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0186, + "steps": 23 } diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/79eb15660c78742aed7621a6dd68b527.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/79eb15660c78742aed7621a6dd68b527.json new file mode 100644 index 0000000000000000000000000000000000000000..e886fc370aacf62b109068ef8eab40d9611ba397 --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.0.session/cache/79eb15660c78742aed7621a6dd68b527.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0225, + "steps": 34 } diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/62ebc7446153c03392e768f156775a04.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/62ebc7446153c03392e768f156775a04.json new file mode 100644 index 0000000000000000000000000000000000000000..66a7393b502d0c99e1045764f2d0e27f9bba9153 --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/62ebc7446153c03392e768f156775a04.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0178, + "steps": 25 } diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/f4a2b5ec3ce22173881bed69a80a352d.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/f4a2b5ec3ce22173881bed69a80a352d.json new file mode 100644 index 0000000000000000000000000000000000000000..d6ed629ed6503b3493c0b113b01da0d83a0228d8 --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.0.session/cache/f4a2b5ec3ce22173881bed69a80a352d.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0175, + "steps": 23 } diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.session/cache/108580f3feacdb8f5c76cbe017d6adc4.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.session/cache/108580f3feacdb8f5c76cbe017d6adc4.json new file mode 100644 index 0000000000000000000000000000000000000000..b068113a500a291d7ad13df6d1da6e8a62a406d4 --- /dev/null +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.session/cache/108580f3feacdb8f5c76cbe017d6adc4.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0225, + "steps": 44 } diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/32344a2dbed6023a19c79075bb121f6d.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/32344a2dbed6023a19c79075bb121f6d.json new file mode 100644 index 0000000000000000000000000000000000000000..16d19ceb388989d8142fd2c2a7248345ad165cd2 --- /dev/null +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/32344a2dbed6023a19c79075bb121f6d.json @@ -0,0 +1 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "timeout", "time": 10. } diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/9e94bad7226c7a7a4c490b4470893c4e.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/9e94bad7226c7a7a4c490b4470893c4e.json new file mode 100644 index 0000000000000000000000000000000000000000..17b2892ccbf195b145741ac8c4318db535989499 --- /dev/null +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/9e94bad7226c7a7a4c490b4470893c4e.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0111, + "steps": 17 } diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/b7f823b078205dea4e390c65717432a0.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/b7f823b078205dea4e390c65717432a0.json new file mode 100644 index 0000000000000000000000000000000000000000..ebe158e74613db982b06330ac9726e723adc73a2 --- /dev/null +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/frame.0.session/cache/b7f823b078205dea4e390c65717432a0.json @@ -0,0 +1,2 @@ +{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0144, + "steps": 16 }