From 25ae5c39b9f851e867f70755185bd321e81a122c Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Wed, 1 Apr 2020 09:36:21 +0200
Subject: [PATCH 1/2] cleaning
---
.gitignore | 3 ++
bench/ce/jlamp0/why3session.xml | 45 ----------------
bench/ce/jlamp0/why3shapes.gz | Bin 509 -> 0 bytes
bench/ce/let_constant/why3session.xml | 18 -------
bench/ce/let_constant/why3shapes.gz | Bin 138 -> 0 bytes
bench/ce/loop_inv.mlw | 57 +++++++++++++++++++++
bench/ce/threshold.mlw | 28 ++++++++++
examples/bts/353.mlw | 22 ++++++++
examples/bts/374_eliminate_if_explodes.mlw | 25 +++++++++
examples/logic/bvsum.mlw | 28 ++++++++++
examples/logic/bvsum/why3session.xml | 38 ++++++++++++++
examples/logic/bvsum/why3shapes.gz | Bin 0 -> 238 bytes
examples/times2float.mlw | 8 +++
examples/times2float/why3session.xml | 18 +++++++
examples/times2float/why3shapes.gz | Bin 0 -> 114 bytes
15 files changed, 227 insertions(+), 63 deletions(-)
delete mode 100644 bench/ce/jlamp0/why3session.xml
delete mode 100644 bench/ce/jlamp0/why3shapes.gz
delete mode 100644 bench/ce/let_constant/why3session.xml
delete mode 100644 bench/ce/let_constant/why3shapes.gz
create mode 100644 bench/ce/loop_inv.mlw
create mode 100644 bench/ce/threshold.mlw
create mode 100644 examples/bts/353.mlw
create mode 100644 examples/bts/374_eliminate_if_explodes.mlw
create mode 100644 examples/logic/bvsum.mlw
create mode 100644 examples/logic/bvsum/why3session.xml
create mode 100644 examples/logic/bvsum/why3shapes.gz
create mode 100644 examples/times2float.mlw
create mode 100644 examples/times2float/why3session.xml
create mode 100644 examples/times2float/why3shapes.gz
diff --git a/.gitignore b/.gitignore
index 0cc52d1b74..b92c47765d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -118,6 +118,8 @@ why3.conf
/doc/_build
/doc/.doctrees/
+/public/
+
# /lib
/lib/why3-cpulimit
/lib/why3-cpulimit.exe
@@ -247,6 +249,7 @@ pvsbin/
/tests/microc/*/why3shapes.gz
# /examples/
+/examples/use_api/results
/examples/in_progress/course/
/examples/in_progress/wcet_hull/
/examples/in_progress/binary_search2/
diff --git a/bench/ce/jlamp0/why3session.xml b/bench/ce/jlamp0/why3session.xml
deleted file mode 100644
index 35a1e652b9..0000000000
--- a/bench/ce/jlamp0/why3session.xml
+++ /dev/null
@@ -1,45 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
-"http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="4">
-<prover id="0" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../jlamp0.mlw">
-<theory name="M">
- <goal name="WP_parameter p1" expl="VC for p1">
- <transf name="split_vc" >
- <goal name="WP_parameter p1.0" expl="assertion">
- <proof prover="0"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="WP_parameter p1.1" expl="postcondition">
- <proof prover="0"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="WP_parameter p1.2" expl="postcondition">
- <proof prover="0"><result status="unknown" time="0.02"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="WP_parameter p2" expl="VC for p2">
- <transf name="split_vc" >
- <goal name="WP_parameter p2.0" expl="loop invariant init">
- <proof prover="0"><result status="unknown" time="0.00"/></proof>
- </goal>
- <goal name="WP_parameter p2.1" expl="loop invariant init">
- <proof prover="0"><result status="unknown" time="0.00"/></proof>
- </goal>
- <goal name="WP_parameter p2.2" expl="loop invariant preservation">
- <proof prover="0"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="WP_parameter p2.3" expl="loop invariant preservation">
- <proof prover="0"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="WP_parameter p2.4" expl="loop variant decrease">
- <proof prover="0"><result status="unknown" time="0.00"/></proof>
- </goal>
- <goal name="WP_parameter p2.5" expl="postcondition">
- <proof prover="0"><result status="unknown" time="0.00"/></proof>
- </goal>
- </transf>
- </goal>
-</theory>
-</file>
-</why3session>
diff --git a/bench/ce/jlamp0/why3shapes.gz b/bench/ce/jlamp0/why3shapes.gz
deleted file mode 100644
index 9111c10989c36406dbd33fe4bca490ec438518a3..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001
literal 509
zcmb2|=3oGW|5GR5?vgg-X?y=&^VvQTou3N)Z^WDu6XFki-=uQb!P7}-nqA%8Nxo@m
z+n4U$tn=mN7j2`f6HK=mnzdgIobn>;vf$ROcRmH|<9}Nq)o1W|PyXlg4}UIQz;frV
zFQe9vf?xc8|Er95fByFCmZZVmp8Rm79e0fwkFY9>)hOHxuGI{<^W_&uk?nP*6Vp`%
z!#IzK&RDjbEtzMfRzT9#Iocad*iO_kom^`5;b+eB(=|8lE6+4vYG^;P#X*U;aZc*$
zh=cuRK^+0UwmioV|5R$<doKD)TF~65#v4{&TlAcTQ7dAa;LH_iMJiwHbwaqW1({5D
zaMjk#{M;KYbnxQE+U*wq3u{Z_Zx+AIj_55&oVsD&di}(QJxm)4k~;fKkNvg^EU5a^
z{(HZ^#o8qg<EB5&`}AvT&$Y_JTe@FAEr}JAniNnVrr1BjCgRIXx1a|R?egu13uk=K
zubEX@|8o7$PcwGre7Mu7_~qxf6Q|BTUv=-7HLJ5p4(H+fje9bey}z*ZimB9GmG%%x
z&GOiko|7t#&i9!5)n8AleZ1AmZsiou*1Mq@>%6Yjy^2~Nu0KV_{Lh77&mZ_}eY<-6
z)e`gnzh^8mzMzxzLiS14cELT#SD&QRY%6EuJ{^>@_mbhUYge{d&NotQ5irq6H<0dq
U5byt}N^n0zhVDd-cPtDH0BsNd;Q#;t
diff --git a/bench/ce/let_constant/why3session.xml b/bench/ce/let_constant/why3session.xml
deleted file mode 100644
index 124d1cb0ef..0000000000
--- a/bench/ce/let_constant/why3session.xml
+++ /dev/null
@@ -1,18 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
-"http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="8">
-<prover id="0" name="CVC4" version="1.5" alternative="counterexamples" timelimit="5" steplimit="0" memlimit="1000"/>
-<file>
-<path name=".."/><path name="let_constant.mlw"/>
-<theory name="Let_constant">
- <goal name="VC dummy" expl="VC for dummy">
- <transf name="split_vc" >
- <goal name="VC dummy.0" expl="assertion">
- <proof prover="0"><result status="unknown" time="0.01" steps="286"/></proof>
- </goal>
- </transf>
- </goal>
-</theory>
-</file>
-</why3session>
diff --git a/bench/ce/let_constant/why3shapes.gz b/bench/ce/let_constant/why3shapes.gz
deleted file mode 100644
index e5887072365ca4a372561f2b5754cc2597119061..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001
literal 138
zcmb2|=3oGW|GFm(`3@QIFdVqM{=~T?^=;m5n-ms)Xnfaq*@I_k5I6Jw<xV-vH(xxn
zxFPmUiN{e-ft>r#-+qmlzkmLR|K-yB?mG{b@YddSs@6Zve!#%^R>K|5Or=+bPvaKz
s)r19oJ)qk7JnIOrw%PTWN3(k`RSBz_zmrK?*z|$*lyB|ri3|)302y~ckN^Mx
diff --git a/bench/ce/loop_inv.mlw b/bench/ce/loop_inv.mlw
new file mode 100644
index 0000000000..ebf4caf28b
--- /dev/null
+++ b/bench/ce/loop_inv.mlw
@@ -0,0 +1,57 @@
+
+module M
+
+use int.Int
+
+let f () =
+ let ref a = 0 in
+ a <- 1;
+ let ref b = 2 in
+ while b < 10 do
+ invariant { b < a + 5 }
+ b <- a + b
+ done
+
+end
+
+module N
+
+use int.Int
+
+val ref a : int
+
+val ref b : int
+
+let f () : int
+ ensures { result < a }
+ =
+ a <- 1;
+ b <- 2;
+ while b < 10 do
+ invariant { b < a + 5 }
+ b <- a + b
+ done;
+ b
+
+end
+
+module R
+
+use real.Real
+
+val ref a : real
+
+val ref b : real
+
+let f () : real
+ ensures { result < a }
+ =
+ a <- 1.0;
+ b <- 2.0;
+ while b < 10.0 do
+ invariant { b < a + 5.0 }
+ b <- a + b
+ done;
+ b
+
+end
diff --git a/bench/ce/threshold.mlw b/bench/ce/threshold.mlw
new file mode 100644
index 0000000000..17294e4f5a
--- /dev/null
+++ b/bench/ce/threshold.mlw
@@ -0,0 +1,28 @@
+
+module WithInt32
+use int.Int
+use mach.int.Int32
+
+
+let f (n min max:int32) : int32
+ ensures { min <= result <= max }
+=
+ let x = min + max in
+ if n < min then min else if n > max then max else n
+
+end
+
+module WithBV32
+use int.Int
+use bv.BV32
+use mach.bv.BVCheck32
+
+
+let f (n min max:BV32.t) : BV32.t
+ ensures { ule min result /\ ule result max }
+ (* ensures { BV32.t'int min <= BV32.t'int result <= BV32.t'int max } *)
+=
+ let x = add_check min max in
+ if lt_check n min then min else if gt_check n max then max else n
+
+end
diff --git a/examples/bts/353.mlw b/examples/bts/353.mlw
new file mode 100644
index 0000000000..c15f24772f
--- /dev/null
+++ b/examples/bts/353.mlw
@@ -0,0 +1,22 @@
+
+module M
+
+ use int.Int
+ use ref.Ref
+
+ let f (a: ref int)
+ requires { !a = 42 }
+ ensures { !a = 2 + old !a + result } =
+ a := 0;
+ a := 1;
+ !a+1
+
+ let g (a: ref int)
+ requires { !a = 42 }
+ ensures { !a = 2 + old !a + result } =
+ a := 0;
+ a := 1;
+ let b = !a + !a in
+ b+1
+
+end
\ No newline at end of file
diff --git a/examples/bts/374_eliminate_if_explodes.mlw b/examples/bts/374_eliminate_if_explodes.mlw
new file mode 100644
index 0000000000..e61bbbf0b5
--- /dev/null
+++ b/examples/bts/374_eliminate_if_explodes.mlw
@@ -0,0 +1,25 @@
+module Lexer__read_token__subprogram_def
+ use "int".Int
+ use bool.Bool
+
+ exception Exc7
+ exception Exc4
+
+ val c : int
+
+ let def ()
+ =
+ try
+ if c = 40 then ()
+ else if c = 41 then ()
+ else if c = 121 then ()
+ else if c = 35 then ()
+ else if andb (48 <= c) (c <= 57)then ()
+ else if orb (orb (andb (65 <= c) (c <= 90)) (andb (97 <= c) (c <= 122))) (orb (orb (orb (orb (orb (orb (andb (33 <= c) (c <= 33)) (andb (36 <= c) (c <= 38))) (andb (42 <= c) (c <= 43))) (andb (45 <= c) (c <= 47))) (andb (60 <= c) (c <= 64))) (andb (94 <= c) (c <= 95))) (andb (126 <= c) (c <= 126))) then raise Exc7
+ else if c = 34 then raise Exc4 else ();
+ with
+ | Exc4 -> ()
+ | Exc7 -> ()
+ end;
+ assert { false }
+end
diff --git a/examples/logic/bvsum.mlw b/examples/logic/bvsum.mlw
new file mode 100644
index 0000000000..2eb50694f6
--- /dev/null
+++ b/examples/logic/bvsum.mlw
@@ -0,0 +1,28 @@
+
+module PureBV
+
+use bv.BV32
+
+lemma add_bv : forall x y. add x y = add (bw_and x y) (bw_or x y)
+
+goal g : forall x y z.
+ add (add x y) z = add (bw_and (add (bw_and x y) (bw_or x y)) z) (bw_or (add (bw_and x y) (bw_or x y)) z)
+
+end
+
+module Mixed
+
+use bv.BV32
+use int.Int
+
+lemma add_bv : forall x y. add x y = add (bw_and x y) (bw_or x y)
+
+lemma add_bv_int : forall x y. to_int x + to_int y = to_int (bw_and x y) + to_int (bw_or x y)
+
+(*
+goal g : forall x y z.
+ to_int x + to_int y + to_int z = (bw_and (add (bw_and x y) (bw_or x y)) z) (bw_or (add (bw_and x y) (bw_or x y)) z)
+*)
+
+end
+
diff --git a/examples/logic/bvsum/why3session.xml b/examples/logic/bvsum/why3session.xml
new file mode 100644
index 0000000000..126684f6df
--- /dev/null
+++ b/examples/logic/bvsum/why3session.xml
@@ -0,0 +1,38 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="6">
+<prover id="0" name="Z3" version="4.8.4" timelimit="10" steplimit="0" memlimit="4000"/>
+<prover id="1" name="CVC4" version="1.6" alternative="counterexamples" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Z3" version="4.8.4" alternative="counterexamples" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.3.0" timelimit="10" steplimit="0" memlimit="4000"/>
+<prover id="4" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
+<file>
+<path name=".."/><path name="bvsum.mlw"/>
+<theory name="PureBV" proved="true">
+ <goal name="add_bv" proved="true">
+ <proof prover="4"><result status="valid" time="0.05" steps="13986"/></proof>
+ </goal>
+ <goal name="g" proved="true">
+ <proof prover="4"><result status="valid" time="0.08" steps="31108"/></proof>
+ </goal>
+</theory>
+<theory name="Mixed">
+ <goal name="add_bv" proved="true">
+ <proof prover="4"><result status="valid" time="0.03" steps="13986"/></proof>
+ </goal>
+ <goal name="add_bv_int">
+ <proof prover="1"><result status="timeout" time="1.00" steps="258185"/></proof>
+ <proof prover="2"><result status="timeout" time="1.00"/></proof>
+ <proof prover="3" timelimit="1" memlimit="1000"><result status="timeout" time="1.00"/></proof>
+ <transf name="split_vc" >
+ <goal name="add_bv_int.0">
+ <proof prover="0"><result status="timeout" time="10.00"/></proof>
+ <proof prover="3"><result status="timeout" time="10.00"/></proof>
+ <proof prover="4" timelimit="10" memlimit="4000"><result status="timeout" time="10.00" steps="3358556"/></proof>
+ </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/logic/bvsum/why3shapes.gz b/examples/logic/bvsum/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..d6f9d79e156ae1043233936a01f4d25b00b5ccc3
GIT binary patch
literal 238
zcmb2|=3oGW|GoVi^9~#ExRlqre%G7i5&Y@G)feI!rW&0t)+U@$%)bBjZJDg#*1l-6
z-|}+zuJ{?%`ukeGKKW()`C*l5<)4_VPo6y967y`mxn1XD-3_ftjZM36>^pcbk2gH)
zay`T4s6S^;7uMP9)a>g%eR%g-i`m}`)?DtX-F9Sm!~L7N&+K+fO)id9ekx`ukg4?I
zq@C$9HZO({=Nhi{_gt0wSN@XHy5^^4$`=>v&e<Wc%kkod`qET~hg||}8On=<lsXGu
s&s=OK*nGjjOEPHEz0RZG^=8dtx94%#=G~egA@PlQXWaXnhZz|d03DETng9R*
literal 0
HcmV?d00001
diff --git a/examples/times2float.mlw b/examples/times2float.mlw
new file mode 100644
index 0000000000..c86dc5f6c6
--- /dev/null
+++ b/examples/times2float.mlw
@@ -0,0 +1,8 @@
+
+
+use ieee_float.Float32
+
+let f (x: Float32.t) : Float32.t
+ requires { lt (0.0:t) x /\ lt x (1000.0:t) }
+ ensures { not (eq (add RNE x x) result) }
+ = mul RNE x (2.0:Float32.t)
diff --git a/examples/times2float/why3session.xml b/examples/times2float/why3session.xml
new file mode 100644
index 0000000000..b1fcc983a3
--- /dev/null
+++ b/examples/times2float/why3session.xml
@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="6">
+<prover id="0" name="CVC4" version="1.7" alternative="counterexamples" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.8.4" alternative="counterexamples" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.3.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<file format="whyml">
+<path name=".."/><path name="times2float.mlw"/>
+<theory name="Top">
+ <goal name="f'vc" expl="VC for f">
+ <proof prover="0"><result status="timeout" time="5.00" steps="2009908"/></proof>
+ <proof prover="1"><result status="unknown" time="0.14" steps="387381"/></proof>
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/times2float/why3shapes.gz b/examples/times2float/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..b0553e5d0d73450924907d79be0b3801550f30a4
GIT binary patch
literal 114
zcmb2|=3oGW|GHhL`5X)c7~cQws%w06YlT&pfS#?zmwnsbc2>0fSKo0q<yhgJna&R`
zZk4n7P;^$FJ53<*aO3mO=C@YV`8?1)e^>MVi!E|inn&3T&5yQB<IvVTmGUV?`RGZG
S+X_<E0p@&4a`O2M3=9B#yfOg*
literal 0
HcmV?d00001
--
GitLab
From 00007fd0021a319ab48e876294685b53ae2969dc Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Thu, 2 Apr 2020 10:55:18 +0200
Subject: [PATCH 2/2] Adding missing oracles for counterexamples
---
bench/ce/loop_inv.mlw | 6 +-
bench/ce/oracles/loop_inv_CVC4,1.7_SP.oracle | 89 +++++++++++++++++++
bench/ce/oracles/loop_inv_CVC4,1.7_WP.oracle | 89 +++++++++++++++++++
bench/ce/oracles/loop_inv_Z3,4.8.4_SP.oracle | 89 +++++++++++++++++++
bench/ce/oracles/loop_inv_Z3,4.8.4_WP.oracle | 89 +++++++++++++++++++
bench/ce/oracles/threshold_CVC4,1.7_SP.oracle | 69 ++++++++++++++
bench/ce/oracles/threshold_CVC4,1.7_WP.oracle | 69 ++++++++++++++
bench/ce/oracles/threshold_Z3,4.8.4_SP.oracle | 65 ++++++++++++++
bench/ce/oracles/threshold_Z3,4.8.4_WP.oracle | 65 ++++++++++++++
bench/ce/threshold.mlw | 4 +-
10 files changed, 631 insertions(+), 3 deletions(-)
create mode 100644 bench/ce/oracles/loop_inv_CVC4,1.7_SP.oracle
create mode 100644 bench/ce/oracles/loop_inv_CVC4,1.7_WP.oracle
create mode 100644 bench/ce/oracles/loop_inv_Z3,4.8.4_SP.oracle
create mode 100644 bench/ce/oracles/loop_inv_Z3,4.8.4_WP.oracle
create mode 100644 bench/ce/oracles/threshold_CVC4,1.7_SP.oracle
create mode 100644 bench/ce/oracles/threshold_CVC4,1.7_WP.oracle
create mode 100644 bench/ce/oracles/threshold_Z3,4.8.4_SP.oracle
create mode 100644 bench/ce/oracles/threshold_Z3,4.8.4_WP.oracle
diff --git a/bench/ce/loop_inv.mlw b/bench/ce/loop_inv.mlw
index ebf4caf28b..ab17db4830 100644
--- a/bench/ce/loop_inv.mlw
+++ b/bench/ce/loop_inv.mlw
@@ -3,7 +3,9 @@ module M
use int.Int
-let f () =
+let f () : unit
+ diverges
+ =
let ref a = 0 in
a <- 1;
let ref b = 2 in
@@ -23,6 +25,7 @@ val ref a : int
val ref b : int
let f () : int
+ diverges
ensures { result < a }
=
a <- 1;
@@ -44,6 +47,7 @@ val ref a : real
val ref b : real
let f () : real
+ diverges
ensures { result < a }
=
a <- 1.0;
diff --git a/bench/ce/oracles/loop_inv_CVC4,1.7_SP.oracle b/bench/ce/oracles/loop_inv_CVC4,1.7_SP.oracle
new file mode 100644
index 0000000000..e5ab8447a5
--- /dev/null
+++ b/bench/ce/oracles/loop_inv_CVC4,1.7_SP.oracle
@@ -0,0 +1,89 @@
+Strongest Postcondition
+bench/ce/loop_inv.mlw M f'vc: Valid
+bench/ce/loop_inv.mlw M f'vc: Unknown (sat)
+Counter-example model:
+File loop_inv.mlw:
+ Line 10:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ Line 12:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "5" } }] } }
+ Line 13:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+ Line 14:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+
+bench/ce/loop_inv.mlw N f'vc: Valid
+bench/ce/loop_inv.mlw N f'vc: Unknown (sat)
+Counter-example model:
+File loop_inv.mlw:
+ Line 31:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ Line 32:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "2" } }] } }
+ Line 33:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "5" } }] } }
+ Line 34:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+ Line 35:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+
+bench/ce/loop_inv.mlw N f'vc: Valid
+bench/ce/loop_inv.mlw R f'vc: Valid
+bench/ce/loop_inv.mlw R f'vc: Timeout or Unknown
+Counter-example model:
+File loop_inv.mlw:
+ Line 53:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "1.0" } }] } }
+ Line 54:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "2.0" } }] } }
+ Line 55:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "5.0" } }] } }
+ Line 56:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "1.0" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "6.0" } }] } }
+ Line 57:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "6.0" } }] } }
+
+bench/ce/loop_inv.mlw R f'vc: Valid
diff --git a/bench/ce/oracles/loop_inv_CVC4,1.7_WP.oracle b/bench/ce/oracles/loop_inv_CVC4,1.7_WP.oracle
new file mode 100644
index 0000000000..709dae3f34
--- /dev/null
+++ b/bench/ce/oracles/loop_inv_CVC4,1.7_WP.oracle
@@ -0,0 +1,89 @@
+Weakest Precondition
+bench/ce/loop_inv.mlw M f'vc: Valid
+bench/ce/loop_inv.mlw M f'vc: Unknown (sat)
+Counter-example model:
+File loop_inv.mlw:
+ Line 10:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ Line 12:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "5" } }] } }
+ Line 13:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+ Line 14:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+
+bench/ce/loop_inv.mlw N f'vc: Valid
+bench/ce/loop_inv.mlw N f'vc: Unknown (sat)
+Counter-example model:
+File loop_inv.mlw:
+ Line 31:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ Line 32:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "2" } }] } }
+ Line 33:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "5" } }] } }
+ Line 34:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+ Line 35:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+
+bench/ce/loop_inv.mlw N f'vc: Valid
+bench/ce/loop_inv.mlw R f'vc: Valid
+bench/ce/loop_inv.mlw R f'vc: Timeout or Unknown
+Counter-example model:
+File loop_inv.mlw:
+ Line 53:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "1.0" } }] } }
+ Line 54:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "2.0" } }] } }
+ Line 55:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "5.0" } }] } }
+ Line 56:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "1.0" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "6.0" } }] } }
+ Line 57:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "6.0" } }] } }
+
+bench/ce/loop_inv.mlw R f'vc: Valid
diff --git a/bench/ce/oracles/loop_inv_Z3,4.8.4_SP.oracle b/bench/ce/oracles/loop_inv_Z3,4.8.4_SP.oracle
new file mode 100644
index 0000000000..c313de70fc
--- /dev/null
+++ b/bench/ce/oracles/loop_inv_Z3,4.8.4_SP.oracle
@@ -0,0 +1,89 @@
+Strongest Postcondition
+bench/ce/loop_inv.mlw M f'vc: Valid
+bench/ce/loop_inv.mlw M f'vc: Timeout or Unknown
+Counter-example model:
+File loop_inv.mlw:
+ Line 10:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ Line 12:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "5" } }] } }
+ Line 13:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+ Line 14:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+
+bench/ce/loop_inv.mlw N f'vc: Valid
+bench/ce/loop_inv.mlw N f'vc: Timeout or Unknown
+Counter-example model:
+File loop_inv.mlw:
+ Line 31:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ Line 32:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "2" } }] } }
+ Line 33:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "5" } }] } }
+ Line 34:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+ Line 35:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+
+bench/ce/loop_inv.mlw N f'vc: Valid
+bench/ce/loop_inv.mlw R f'vc: Valid
+bench/ce/loop_inv.mlw R f'vc: Timeout or Unknown
+Counter-example model:
+File loop_inv.mlw:
+ Line 53:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "1.0" } }] } }
+ Line 54:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "2.0" } }] } }
+ Line 55:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "5.0" } }] } }
+ Line 56:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "1.0" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "6.0" } }] } }
+ Line 57:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "6.0" } }] } }
+
+bench/ce/loop_inv.mlw R f'vc: Valid
diff --git a/bench/ce/oracles/loop_inv_Z3,4.8.4_WP.oracle b/bench/ce/oracles/loop_inv_Z3,4.8.4_WP.oracle
new file mode 100644
index 0000000000..0b89b34700
--- /dev/null
+++ b/bench/ce/oracles/loop_inv_Z3,4.8.4_WP.oracle
@@ -0,0 +1,89 @@
+Weakest Precondition
+bench/ce/loop_inv.mlw M f'vc: Valid
+bench/ce/loop_inv.mlw M f'vc: Timeout or Unknown
+Counter-example model:
+File loop_inv.mlw:
+ Line 10:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ Line 12:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "5" } }] } }
+ Line 13:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+ Line 14:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+
+bench/ce/loop_inv.mlw N f'vc: Valid
+bench/ce/loop_inv.mlw N f'vc: Timeout or Unknown
+Counter-example model:
+File loop_inv.mlw:
+ Line 31:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ Line 32:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "2" } }] } }
+ Line 33:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "5" } }] } }
+ Line 34:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+ Line 35:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Integer" , "val" : "6" } }] } }
+
+bench/ce/loop_inv.mlw N f'vc: Valid
+bench/ce/loop_inv.mlw R f'vc: Valid
+bench/ce/loop_inv.mlw R f'vc: Timeout or Unknown
+Counter-example model:
+File loop_inv.mlw:
+ Line 53:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "1.0" } }] } }
+ Line 54:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "2.0" } }] } }
+ Line 55:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "5.0" } }] } }
+ Line 56:
+ a, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:a]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "1.0" } }] } }
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+ [@model_trace:b]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "6.0" } }] } }
+ Line 57:
+ b, [[@mlw:reference_var], [@introduced], [@field:0:contents]] =
+ {"type" : "Record" , "val" : {"Field" : [{"field" : "contents" ,
+ "value" : {"type" : "Decimal" , "val" : "6.0" } }] } }
+
+bench/ce/loop_inv.mlw R f'vc: Valid
diff --git a/bench/ce/oracles/threshold_CVC4,1.7_SP.oracle b/bench/ce/oracles/threshold_CVC4,1.7_SP.oracle
new file mode 100644
index 0000000000..0d8e6346eb
--- /dev/null
+++ b/bench/ce/oracles/threshold_CVC4,1.7_SP.oracle
@@ -0,0 +1,69 @@
+Strongest Postcondition
+bench/ce/threshold.mlw WithInt32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 7:
+ max, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1073741825" } }
+ min, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1073741825" } }
+ n, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1073741825" } }
+ Line 10:
+ max, [[@introduced], [@model_trace:max]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" ,
+ "val" : "-1073741825" } }
+ min, [[@introduced], [@model_trace:min]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" ,
+ "val" : "-1073741825" } }
+
+bench/ce/threshold.mlw WithInt32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 7:
+ max, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+ min, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "0" } }
+ n, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "0" } }
+ Line 8:
+ max, [[@introduced], [@model_trace:max]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "-1" } }
+ min, [[@introduced], [@model_trace:min]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } }
+ result, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+ Line 10:
+ _x, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+
+bench/ce/threshold.mlw WithBV32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 21:
+ max, [[@introduced]] = {"type" : "Integer" , "val" : "4294967295" }
+ min, [[@introduced]] = {"type" : "Integer" , "val" : "4294967295" }
+ n, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
+ Line 25:
+ max, [[@introduced], [@model_trace:max]] = {"type" : "Integer" ,
+ "val" : "4294967295" }
+ min, [[@introduced], [@model_trace:min]] = {"type" : "Integer" ,
+ "val" : "4294967295" }
+
+bench/ce/threshold.mlw WithBV32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 21:
+ max, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
+ min, [[@introduced]] = {"type" : "Integer" , "val" : "1" }
+ n, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
+ Line 22:
+ max, [[@introduced], [@model_trace:max]] = {"type" : "Integer" ,
+ "val" : "0" }
+ min, [[@introduced], [@model_trace:min]] = {"type" : "Integer" ,
+ "val" : "1" }
+ result, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
+ Line 25:
+ _x, [[@introduced]] = {"type" : "Integer" , "val" : "1" }
+
diff --git a/bench/ce/oracles/threshold_CVC4,1.7_WP.oracle b/bench/ce/oracles/threshold_CVC4,1.7_WP.oracle
new file mode 100644
index 0000000000..532c7db12c
--- /dev/null
+++ b/bench/ce/oracles/threshold_CVC4,1.7_WP.oracle
@@ -0,0 +1,69 @@
+Weakest Precondition
+bench/ce/threshold.mlw WithInt32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 7:
+ max, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1073741825" } }
+ min, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1073741825" } }
+ n, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1073741825" } }
+ Line 10:
+ max, [[@introduced], [@model_trace:max]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" ,
+ "val" : "-1073741825" } }
+ min, [[@introduced], [@model_trace:min]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" ,
+ "val" : "-1073741825" } }
+
+bench/ce/threshold.mlw WithInt32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 7:
+ max, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+ min, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "0" } }
+ n, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "0" } }
+ Line 8:
+ max, [[@introduced], [@model_trace:max]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "-1" } }
+ min, [[@introduced], [@model_trace:min]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } }
+ result, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+ Line 10:
+ _x, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+
+bench/ce/threshold.mlw WithBV32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 21:
+ max, [[@introduced]] = {"type" : "Integer" , "val" : "4294967295" }
+ min, [[@introduced]] = {"type" : "Integer" , "val" : "4294967295" }
+ n, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
+ Line 25:
+ max, [[@introduced], [@model_trace:max]] = {"type" : "Integer" ,
+ "val" : "4294967295" }
+ min, [[@introduced], [@model_trace:min]] = {"type" : "Integer" ,
+ "val" : "4294967295" }
+
+bench/ce/threshold.mlw WithBV32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 21:
+ max, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
+ min, [[@introduced]] = {"type" : "Integer" , "val" : "1" }
+ n, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
+ Line 22:
+ max, [[@introduced], [@model_trace:max]] = {"type" : "Integer" ,
+ "val" : "0" }
+ min, [[@introduced], [@model_trace:min]] = {"type" : "Integer" ,
+ "val" : "1" }
+ result, [[@introduced]] = {"type" : "Integer" , "val" : "0" }
+ Line 25:
+ _x, [[@introduced]] = {"type" : "Integer" , "val" : "1" }
+
diff --git a/bench/ce/oracles/threshold_Z3,4.8.4_SP.oracle b/bench/ce/oracles/threshold_Z3,4.8.4_SP.oracle
new file mode 100644
index 0000000000..7d4892186d
--- /dev/null
+++ b/bench/ce/oracles/threshold_Z3,4.8.4_SP.oracle
@@ -0,0 +1,65 @@
+Strongest Postcondition
+bench/ce/threshold.mlw WithInt32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 7:
+ max, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }
+ min, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "2147483647" } }
+ Line 10:
+ max, [[@introduced], [@model_trace:max]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "1" } }
+ min, [[@introduced], [@model_trace:min]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" ,
+ "val" : "2147483647" } }
+
+bench/ce/threshold.mlw WithInt32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 7:
+ max, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+ min, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "0" } }
+ n, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+ Line 8:
+ max, [[@introduced], [@model_trace:max]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "-1" } }
+ min, [[@introduced], [@model_trace:min]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } }
+ result, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "0" } }
+ Line 10:
+ _x, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+
+bench/ce/threshold.mlw WithBV32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 21:
+ max, [[@introduced]] = {"type" : "Integer" , "val" : "4026531703" }
+ min, [[@introduced]] = {"type" : "Integer" , "val" : "4116707090" }
+ Line 25:
+ max, [[@introduced], [@model_trace:max]] = {"type" : "Integer" ,
+ "val" : "4026531703" }
+ min, [[@introduced], [@model_trace:min]] = {"type" : "Integer" ,
+ "val" : "4116707090" }
+
+bench/ce/threshold.mlw WithBV32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 21:
+ max, [[@introduced]] = {"type" : "Integer" , "val" : "1074330528" }
+ min, [[@introduced]] = {"type" : "Integer" , "val" : "1746500513" }
+ n, [[@introduced]] = {"type" : "Integer" , "val" : "1746795424" }
+ Line 22:
+ max, [[@introduced], [@model_trace:max]] = {"type" : "Integer" ,
+ "val" : "1074330528" }
+ min, [[@introduced], [@model_trace:min]] = {"type" : "Integer" ,
+ "val" : "1746500513" }
+ result, [[@introduced]] = {"type" : "Integer" , "val" : "1074330528" }
+ Line 25:
+ _x, [[@introduced]] = {"type" : "Integer" , "val" : "2820831041" }
+
diff --git a/bench/ce/oracles/threshold_Z3,4.8.4_WP.oracle b/bench/ce/oracles/threshold_Z3,4.8.4_WP.oracle
new file mode 100644
index 0000000000..6ad0e0aadf
--- /dev/null
+++ b/bench/ce/oracles/threshold_Z3,4.8.4_WP.oracle
@@ -0,0 +1,65 @@
+Weakest Precondition
+bench/ce/threshold.mlw WithInt32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 7:
+ max, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "1" } }
+ min, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "2147483647" } }
+ Line 10:
+ max, [[@introduced], [@model_trace:max]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "1" } }
+ min, [[@introduced], [@model_trace:min]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" ,
+ "val" : "2147483647" } }
+
+bench/ce/threshold.mlw WithInt32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 7:
+ max, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+ min, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "0" } }
+ n, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+ Line 8:
+ max, [[@introduced], [@model_trace:max]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "-1" } }
+ min, [[@introduced], [@model_trace:min]] = {"proj_name" : "int32'int" ,
+ "type" : "Proj" , "value" : {"type" : "Integer" , "val" : "0" } }
+ result, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "0" } }
+ Line 10:
+ _x, [[@introduced]] = {"proj_name" : "int32'int" , "type" : "Proj" ,
+ "value" : {"type" : "Integer" , "val" : "-1" } }
+
+bench/ce/threshold.mlw WithBV32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 21:
+ max, [[@introduced]] = {"type" : "Integer" , "val" : "4026531703" }
+ min, [[@introduced]] = {"type" : "Integer" , "val" : "4116707090" }
+ Line 25:
+ max, [[@introduced], [@model_trace:max]] = {"type" : "Integer" ,
+ "val" : "4026531703" }
+ min, [[@introduced], [@model_trace:min]] = {"type" : "Integer" ,
+ "val" : "4116707090" }
+
+bench/ce/threshold.mlw WithBV32 f'vc: Timeout or Unknown
+Counter-example model:
+File threshold.mlw:
+ Line 21:
+ max, [[@introduced]] = {"type" : "Integer" , "val" : "1074330528" }
+ min, [[@introduced]] = {"type" : "Integer" , "val" : "1746500513" }
+ n, [[@introduced]] = {"type" : "Integer" , "val" : "1746795424" }
+ Line 22:
+ max, [[@introduced], [@model_trace:max]] = {"type" : "Integer" ,
+ "val" : "1074330528" }
+ min, [[@introduced], [@model_trace:min]] = {"type" : "Integer" ,
+ "val" : "1746500513" }
+ result, [[@introduced]] = {"type" : "Integer" , "val" : "1074330528" }
+ Line 25:
+ _x, [[@introduced]] = {"type" : "Integer" , "val" : "2820831041" }
+
diff --git a/bench/ce/threshold.mlw b/bench/ce/threshold.mlw
index 17294e4f5a..1f0cc5a93b 100644
--- a/bench/ce/threshold.mlw
+++ b/bench/ce/threshold.mlw
@@ -7,7 +7,7 @@ use mach.int.Int32
let f (n min max:int32) : int32
ensures { min <= result <= max }
=
- let x = min + max in
+ let _x = min + max in
if n < min then min else if n > max then max else n
end
@@ -22,7 +22,7 @@ let f (n min max:BV32.t) : BV32.t
ensures { ule min result /\ ule result max }
(* ensures { BV32.t'int min <= BV32.t'int result <= BV32.t'int max } *)
=
- let x = add_check min max in
+ let _x = add_check min max in
if lt_check n min then min else if gt_check n max then max else n
end
--
GitLab