diff --git a/tests/bugs/oracle/issue27-pred.res.oracle b/tests/bugs/oracle/issue27-pred.res.oracle index 4426e1c01ff378c8ff083b3a15ab573a9c4ef658..243ba4370ef7d85c4da9ca05a51b73719c91e0dc 100644 --- a/tests/bugs/oracle/issue27-pred.res.oracle +++ b/tests/bugs/oracle/issue27-pred.res.oracle @@ -4,8 +4,8 @@ Now output intermediate result [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 2 goals scheduled -[wp] [Alt-Ergo] Goal typed_Z3posi_ensures : Valid [wp] [Alt-Ergo] Goal typed_Z3posi_ensures_2 : Valid +[wp] [Alt-Ergo] Goal typed_Z3posi_ensures : Valid [wp] Proved goals: 2 / 2 Qed: 0 Alt-Ergo: 2 diff --git a/tests/wp-cache/cache/2f7a37f471889e53309478f7111f2e3b.json b/tests/wp-cache/cache/2f7a37f471889e53309478f7111f2e3b.json new file mode 100644 index 0000000000000000000000000000000000000000..8ef448a8d3730ba9b40a011375dc10ea9a40f657 --- /dev/null +++ b/tests/wp-cache/cache/2f7a37f471889e53309478f7111f2e3b.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0087, + "steps": 5 } diff --git a/tests/wp-cache/cache/349453e3fffbad07325f8bf5b3443b23.json b/tests/wp-cache/cache/349453e3fffbad07325f8bf5b3443b23.json new file mode 100644 index 0000000000000000000000000000000000000000..30d76e3231464fdb66e346c08d68f4f70cf8975f --- /dev/null +++ b/tests/wp-cache/cache/349453e3fffbad07325f8bf5b3443b23.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0098, + "steps": 4 } diff --git a/tests/wp-cache/cache/88256e17ad3e563fabf4a3938c3414a4.json b/tests/wp-cache/cache/88256e17ad3e563fabf4a3938c3414a4.json new file mode 100644 index 0000000000000000000000000000000000000000..ce94a6ec7175bb17dfef1bf9defcec3c3facb2cf --- /dev/null +++ b/tests/wp-cache/cache/88256e17ad3e563fabf4a3938c3414a4.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0075, + "steps": 7 } diff --git a/tests/wp-cache/cache/90b7ae9827e313e62f15a4c232815006.json b/tests/wp-cache/cache/90b7ae9827e313e62f15a4c232815006.json new file mode 100644 index 0000000000000000000000000000000000000000..3813aaa90d1c325292dcfb7ddaa9ed6fc4351881 --- /dev/null +++ b/tests/wp-cache/cache/90b7ae9827e313e62f15a4c232815006.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0083, + "steps": 6 } diff --git a/tests/wp-cache/cache/a0bac3df4ce0b56c7de3f42bb7e3fdea.json b/tests/wp-cache/cache/a0bac3df4ce0b56c7de3f42bb7e3fdea.json new file mode 100644 index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064 --- /dev/null +++ b/tests/wp-cache/cache/a0bac3df4ce0b56c7de3f42bb7e3fdea.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. } diff --git a/tests/wp-cache/cache/dbf0fd12923e897b3af199827b5edf2b.json b/tests/wp-cache/cache/dbf0fd12923e897b3af199827b5edf2b.json new file mode 100644 index 0000000000000000000000000000000000000000..8256dcea1bc441f80e5f1bc5ffc9ee590a0285ed --- /dev/null +++ b/tests/wp-cache/cache/dbf0fd12923e897b3af199827b5edf2b.json @@ -0,0 +1 @@ +{ "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" } diff --git a/tests/wp-cache/cache/df1d30bf7323b86cce32a6e8fd4c9f58.json b/tests/wp-cache/cache/df1d30bf7323b86cce32a6e8fd4c9f58.json new file mode 100644 index 0000000000000000000000000000000000000000..05f20b89eb41b9b370a36b7696d41dc6ad87d7b8 --- /dev/null +++ b/tests/wp-cache/cache/df1d30bf7323b86cce32a6e8fd4c9f58.json @@ -0,0 +1,2 @@ +{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0135, + "steps": 14 }