From 80780e827d2079e9051bd298738ba26583e2bb8a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 12 Oct 2020 14:34:39 +0200
Subject: [PATCH] update oracle and cache
---
tests/bugs/oracle/issue27-pred.res.oracle | 2 +-
tests/wp-cache/cache/2f7a37f471889e53309478f7111f2e3b.json | 2 ++
tests/wp-cache/cache/349453e3fffbad07325f8bf5b3443b23.json | 2 ++
tests/wp-cache/cache/88256e17ad3e563fabf4a3938c3414a4.json | 2 ++
tests/wp-cache/cache/90b7ae9827e313e62f15a4c232815006.json | 2 ++
tests/wp-cache/cache/a0bac3df4ce0b56c7de3f42bb7e3fdea.json | 1 +
tests/wp-cache/cache/dbf0fd12923e897b3af199827b5edf2b.json | 1 +
tests/wp-cache/cache/df1d30bf7323b86cce32a6e8fd4c9f58.json | 2 ++
8 files changed, 13 insertions(+), 1 deletion(-)
create mode 100644 tests/wp-cache/cache/2f7a37f471889e53309478f7111f2e3b.json
create mode 100644 tests/wp-cache/cache/349453e3fffbad07325f8bf5b3443b23.json
create mode 100644 tests/wp-cache/cache/88256e17ad3e563fabf4a3938c3414a4.json
create mode 100644 tests/wp-cache/cache/90b7ae9827e313e62f15a4c232815006.json
create mode 100644 tests/wp-cache/cache/a0bac3df4ce0b56c7de3f42bb7e3fdea.json
create mode 100644 tests/wp-cache/cache/dbf0fd12923e897b3af199827b5edf2b.json
create mode 100644 tests/wp-cache/cache/df1d30bf7323b86cce32a6e8fd4c9f58.json
diff --git a/tests/bugs/oracle/issue27-pred.res.oracle b/tests/bugs/oracle/issue27-pred.res.oracle
index 4426e1c..243ba43 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 0000000..8ef448a
--- /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 0000000..30d76e3
--- /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 0000000..ce94a6e
--- /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 0000000..3813aaa
--- /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 0000000..b8e36e2
--- /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 0000000..8256dce
--- /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 0000000..05f20b8
--- /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 }
--
GitLab