Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
120
Issues
120
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
4d49b7cd
Commit
4d49b7cd
authored
Oct 10, 2018
by
Sylvain Dailler
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
ce-bench: add sp results
parent
13b02f7e
Changes
41
Hide whitespace changes
Inline
Side-by-side
Showing
41 changed files
with
2159 additions
and
3 deletions
+2159
-3
bench/ce-bench
bench/ce-bench
+12
-3
bench/ce/algebraic_type_CVC4,1.5.oracle
bench/ce/algebraic_type_CVC4,1.5.oracle
+27
-0
bench/ce/algebraic_type_Z3,4.6.0.oracle
bench/ce/algebraic_type_Z3,4.6.0.oracle
+27
-0
bench/ce/array_records_CVC4,1.5.oracle
bench/ce/array_records_CVC4,1.5.oracle
+128
-0
bench/ce/array_records_Z3,4.6.0.oracle
bench/ce/array_records_Z3,4.6.0.oracle
+128
-0
bench/ce/arrays_CVC4,1.5.oracle
bench/ce/arrays_CVC4,1.5.oracle
+7
-0
bench/ce/arrays_Z3,4.6.0.oracle
bench/ce/arrays_Z3,4.6.0.oracle
+7
-0
bench/ce/floats_CVC4,1.5.oracle
bench/ce/floats_CVC4,1.5.oracle
+116
-0
bench/ce/floats_Z3,4.6.0.oracle
bench/ce/floats_Z3,4.6.0.oracle
+205
-0
bench/ce/if_decision_branch_CVC4,1.5.oracle
bench/ce/if_decision_branch_CVC4,1.5.oracle
+11
-0
bench/ce/if_decision_branch_Z3,4.6.0.oracle
bench/ce/if_decision_branch_Z3,4.6.0.oracle
+11
-0
bench/ce/int32_CVC4,1.5.oracle
bench/ce/int32_CVC4,1.5.oracle
+13
-0
bench/ce/int32_Z3,4.6.0.oracle
bench/ce/int32_Z3,4.6.0.oracle
+13
-0
bench/ce/int_CVC4,1.5.oracle
bench/ce/int_CVC4,1.5.oracle
+46
-0
bench/ce/int_Z3,4.6.0.oracle
bench/ce/int_Z3,4.6.0.oracle
+43
-0
bench/ce/int_overflow_CVC4,1.5.oracle
bench/ce/int_overflow_CVC4,1.5.oracle
+106
-0
bench/ce/int_overflow_Z3,4.6.0.oracle
bench/ce/int_overflow_Z3,4.6.0.oracle
+104
-0
bench/ce/jlamp0_CVC4,1.5.oracle
bench/ce/jlamp0_CVC4,1.5.oracle
+72
-0
bench/ce/jlamp0_Z3,4.6.0.oracle
bench/ce/jlamp0_Z3,4.6.0.oracle
+72
-0
bench/ce/jlamp_array_CVC4,1.5.oracle
bench/ce/jlamp_array_CVC4,1.5.oracle
+70
-0
bench/ce/jlamp_array_Z3,4.6.0.oracle
bench/ce/jlamp_array_Z3,4.6.0.oracle
+51
-0
bench/ce/jlamp_projections_CVC4,1.5.oracle
bench/ce/jlamp_projections_CVC4,1.5.oracle
+14
-0
bench/ce/jlamp_projections_Z3,4.6.0.oracle
bench/ce/jlamp_projections_Z3,4.6.0.oracle
+14
-0
bench/ce/list_CVC4,1.5.oracle
bench/ce/list_CVC4,1.5.oracle
+6
-0
bench/ce/list_Z3,4.6.0.oracle
bench/ce/list_Z3,4.6.0.oracle
+6
-0
bench/ce/map_CVC4,1.5.oracle
bench/ce/map_CVC4,1.5.oracle
+87
-0
bench/ce/map_Z3,4.6.0.oracle
bench/ce/map_Z3,4.6.0.oracle
+99
-0
bench/ce/polymorphism_CVC4,1.5.oracle
bench/ce/polymorphism_CVC4,1.5.oracle
+18
-0
bench/ce/polymorphism_Z3,4.6.0.oracle
bench/ce/polymorphism_Z3,4.6.0.oracle
+18
-0
bench/ce/real_CVC4,1.5.oracle
bench/ce/real_CVC4,1.5.oracle
+14
-0
bench/ce/real_Z3,4.6.0.oracle
bench/ce/real_Z3,4.6.0.oracle
+14
-0
bench/ce/record_map_CVC4,1.5.oracle
bench/ce/record_map_CVC4,1.5.oracle
+126
-0
bench/ce/record_map_Z3,4.6.0.oracle
bench/ce/record_map_Z3,4.6.0.oracle
+108
-0
bench/ce/records_CVC4,1.5.oracle
bench/ce/records_CVC4,1.5.oracle
+69
-0
bench/ce/records_Z3,4.6.0.oracle
bench/ce/records_Z3,4.6.0.oracle
+69
-0
bench/ce/ref_CVC4,1.5.oracle
bench/ce/ref_CVC4,1.5.oracle
+79
-0
bench/ce/ref_Z3,4.6.0.oracle
bench/ce/ref_Z3,4.6.0.oracle
+79
-0
bench/ce/result_CVC4,1.5.oracle
bench/ce/result_CVC4,1.5.oracle
+23
-0
bench/ce/result_Z3,4.6.0.oracle
bench/ce/result_Z3,4.6.0.oracle
+23
-0
bench/ce/simple_array_CVC4,1.5.oracle
bench/ce/simple_array_CVC4,1.5.oracle
+12
-0
bench/ce/simple_array_Z3,4.6.0.oracle
bench/ce/simple_array_Z3,4.6.0.oracle
+12
-0
No files found.
bench/ce-bench
View file @
4d49b7cd
...
...
@@ -31,13 +31,24 @@ fi
run
()
{
printf
"
$2
(
$1
)... "
f
=
"
$2_$1
"
printf
"WP
$2
(
$1
)... "
echo
"Weakest Precondition"
>
"
$f
.out"
$dir
/../bin/why3prove.opt
--debug
print_attrs
-P
"
$1
,counterexamples"
--timelimit
1
-a
split_vc
"
$2
.mlw"
|
\
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed
's/ ([0-9]\+\.[0-9]\+s)//'
|
\
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed
-r
's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/'
>
"
$f
.out"
sed
-r
's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/'
>>
"
$f
.out"
printf
"SP
$2
(
$1
)... "
echo
"Strongest Postcondition"
>>
"
$f
.out"
$dir
/../bin/why3prove.opt
--debug
print_attrs
--debug
vc_sp
-P
"
$1
,counterexamples"
--timelimit
1
-a
split_vc
"
$2
.mlw"
|
\
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed
's/ ([0-9]\+\.[0-9]\+s)//'
|
\
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed
-r
's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/'
>>
"
$f
.out"
if
cmp
"
$f
.oracle"
"
$f
.out"
>
/dev/null 2>&1
;
then
echo
"ok"
else
...
...
@@ -53,8 +64,6 @@ run () {
fi
}
for
file
in
$files
;
do
filedir
=
`
dirname
$file
`
filebase
=
`
basename
$file
.mlw
`
...
...
bench/ce/algebraic_type_CVC4,1.5.oracle
View file @
4d49b7cd
Weakest Precondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g2: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Timeout or Unknown
bench/ce/algebraic_type.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "0" },
{"type" : "Integer" ,
"val" : "1" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 6:
...
...
bench/ce/algebraic_type_Z3,4.6.0.oracle
View file @
4d49b7cd
Weakest Precondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat)
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "1" },
{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
Strongest Postcondition
bench/ce/algebraic_type.mlw M G: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 6:
...
...
bench/ce/array_records_CVC4,1.5.oracle
View file @
4d49b7cd
Weakest Precondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
Line 31:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
Strongest Postcondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
...
...
bench/ce/array_records_Z3,4.6.0.oracle
View file @
4d49b7cd
Weakest Precondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-176" }
Line 31:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-176" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-176" }
Line 25:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-176" }
Strongest Postcondition
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout or Unknown
Counter-example model:File array_records.mlw:
Line 23:
...
...
bench/ce/arrays_CVC4,1.5.oracle
View file @
4d49b7cd
Weakest Precondition
bench/ce/arrays.mlw A VC f1: Timeout or Unknown
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Timeout or Unknown
bench/ce/arrays.mlw B VC f1: Timeout or Unknown
bench/ce/arrays.mlw B VC f2: Timeout or Unknown
Strongest Postcondition
bench/ce/arrays.mlw A VC f1: Timeout or Unknown
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Timeout or Unknown
...
...
bench/ce/arrays_Z3,4.6.0.oracle
View file @
4d49b7cd
Weakest Precondition
bench/ce/arrays.mlw A VC f1: Timeout or Unknown
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Timeout or Unknown
bench/ce/arrays.mlw B VC f1: Timeout or Unknown
bench/ce/arrays.mlw B VC f2: Timeout or Unknown
Strongest Postcondition
bench/ce/arrays.mlw A VC f1: Timeout or Unknown
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Timeout or Unknown
...
...
bench/ce/floats_CVC4,1.5.oracle
View file @
4d49b7cd
Weakest Precondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
Strongest Postcondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
...
...
bench/ce/floats_Z3,4.6.0.oracle
View file @
4d49b7cd
Weakest Precondition
bench/ce/floats.mlw T32 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 5:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.000002p-126" ,
"value" : -1.17549e-38 } }
bench/ce/floats.mlw T32 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x0.008000p-127" ,
"value" : -1.14794e-41 } }
bench/ce/floats.mlw T32 g3: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 9:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 11:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.400000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T32 g5: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 13:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.000002p65" ,
"value" : 3.68935e+19 } }
bench/ce/floats.mlw T32 g6: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 15:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 17:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.800000p32" ,
"value" : -6.44245e+09 } }
bench/ce/floats.mlw T32 g8: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 19:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 21:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x0.000002p-127" ,
"value" : 7.00649e-46 } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.99999ap-4" ,
"value" : 0.1 } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 31:
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x1.0000000000001p-1022" ,
"value" : -2.22507e-308 } }
bench/ce/floats.mlw T64 g2: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 222:
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw: