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
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
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
959aa08f
Commit
959aa08f
authored
Sep 05, 2018
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fix sessions for CE bench (more precise 'unknown' answer)
parent
bd8b6aca
Changes
27
Hide whitespace changes
Inline
Side-by-side
Showing
27 changed files
with
101 additions
and
101 deletions
+101
-101
bench/ce/algebraic_type_CVC4,1.5.oracle
bench/ce/algebraic_type_CVC4,1.5.oracle
+1
-1
bench/ce/algebraic_type_Z3,4.6.0.oracle
bench/ce/algebraic_type_Z3,4.6.0.oracle
+1
-1
bench/ce/array_records_CVC4,1.5.oracle
bench/ce/array_records_CVC4,1.5.oracle
+14
-14
bench/ce/arrays_CVC4,1.5.oracle
bench/ce/arrays_CVC4,1.5.oracle
+4
-4
bench/ce/if_decision_branch_CVC4,1.5.oracle
bench/ce/if_decision_branch_CVC4,1.5.oracle
+1
-1
bench/ce/if_decision_branch_Z3,4.6.0.oracle
bench/ce/if_decision_branch_Z3,4.6.0.oracle
+1
-1
bench/ce/int32_CVC4,1.5.oracle
bench/ce/int32_CVC4,1.5.oracle
+1
-1
bench/ce/int_CVC4,1.5.oracle
bench/ce/int_CVC4,1.5.oracle
+4
-4
bench/ce/int_Z3,4.6.0.oracle
bench/ce/int_Z3,4.6.0.oracle
+4
-4
bench/ce/int_overflow_CVC4,1.5.oracle
bench/ce/int_overflow_CVC4,1.5.oracle
+12
-12
bench/ce/int_overflow_Z3,4.6.0.oracle
bench/ce/int_overflow_Z3,4.6.0.oracle
+2
-2
bench/ce/jlamp0_CVC4,1.5.oracle
bench/ce/jlamp0_CVC4,1.5.oracle
+6
-6
bench/ce/jlamp_array_CVC4,1.5.oracle
bench/ce/jlamp_array_CVC4,1.5.oracle
+4
-4
bench/ce/jlamp_projections_CVC4,1.5.oracle
bench/ce/jlamp_projections_CVC4,1.5.oracle
+2
-2
bench/ce/list_CVC4,1.5.oracle
bench/ce/list_CVC4,1.5.oracle
+4
-4
bench/ce/map_CVC4,1.5.oracle
bench/ce/map_CVC4,1.5.oracle
+6
-6
bench/ce/map_Z3,4.6.0.oracle
bench/ce/map_Z3,4.6.0.oracle
+1
-1
bench/ce/real_CVC4,1.5.oracle
bench/ce/real_CVC4,1.5.oracle
+2
-2
bench/ce/real_Z3,4.6.0.oracle
bench/ce/real_Z3,4.6.0.oracle
+2
-2
bench/ce/record_map_CVC4,1.5.oracle
bench/ce/record_map_CVC4,1.5.oracle
+3
-3
bench/ce/record_map_Z3,4.6.0.oracle
bench/ce/record_map_Z3,4.6.0.oracle
+3
-3
bench/ce/records_CVC4,1.5.oracle
bench/ce/records_CVC4,1.5.oracle
+9
-9
bench/ce/records_Z3,4.6.0.oracle
bench/ce/records_Z3,4.6.0.oracle
+4
-4
bench/ce/ref_CVC4,1.5.oracle
bench/ce/ref_CVC4,1.5.oracle
+6
-6
bench/ce/result_CVC4,1.5.oracle
bench/ce/result_CVC4,1.5.oracle
+2
-2
bench/ce/simple_array_CVC4,1.5.oracle
bench/ce/simple_array_CVC4,1.5.oracle
+1
-1
bench/ce/simple_array_Z3,4.6.0.oracle
bench/ce/simple_array_Z3,4.6.0.oracle
+1
-1
No files found.
bench/ce/algebraic_type_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/algebraic_type.mlw M G: Unknown (
other
)
bench/ce/algebraic_type.mlw M G: Unknown (
unknown
)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
...
...
bench/ce/algebraic_type_Z3,4.6.0.oracle
View file @
959aa08f
bench/ce/algebraic_type.mlw M G: Unknown (
other
)
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" ,
...
...
bench/ce/array_records_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -7,7 +7,7 @@ Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -16,7 +16,7 @@ Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -25,7 +25,7 @@ Line 27:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -34,7 +34,7 @@ Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -43,7 +43,7 @@ Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -52,7 +52,7 @@ Line 28:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -61,7 +61,7 @@ Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -70,7 +70,7 @@ Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -79,7 +79,7 @@ Line 29:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -88,7 +88,7 @@ Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -97,7 +97,7 @@ Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -106,7 +106,7 @@ Line 30:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -115,7 +115,7 @@ Line 31:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
other
)
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (
unknown
)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
bench/ce/arrays_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/arrays.mlw A VC f1: Unknown (
other
)
bench/ce/arrays.mlw A VC f1: Unknown (
unknown
)
bench/ce/arrays.mlw A VC f2: Valid
bench/ce/arrays.mlw A VC f2: Unknown (
other
)
bench/ce/arrays.mlw B VC f1: Unknown (
other
)
bench/ce/arrays.mlw B VC f2: Unknown (
other
)
bench/ce/arrays.mlw A VC f2: Unknown (
unknown
)
bench/ce/arrays.mlw B VC f1: Unknown (
unknown
)
bench/ce/arrays.mlw B VC f2: Unknown (
unknown
)
bench/ce/if_decision_branch_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/if_decision_branch.mlw Other VC f: Valid
bench/ce/if_decision_branch.mlw Other VC f: Unknown (
other
)
bench/ce/if_decision_branch.mlw Other VC f: Unknown (
unknown
)
Counter-example model:File if_decision_branch.mlw:
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
...
...
bench/ce/if_decision_branch_Z3,4.6.0.oracle
View file @
959aa08f
bench/ce/if_decision_branch.mlw Other VC f: Valid
bench/ce/if_decision_branch.mlw Other VC f: Unknown (
other
)
bench/ce/if_decision_branch.mlw Other VC f: Unknown (
sat
)
Counter-example model:File if_decision_branch.mlw:
Line 18:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
...
...
bench/ce/int32_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Valid
bench/ce/int32.mlw Ce_int32 VC dummy_update: Unknown (
other
)
bench/ce/int32.mlw Ce_int32 VC dummy_update: Unknown (
unknown
)
Counter-example model:File int32.mlw:
Line 6:
r, [[@introduced], [@model_trace:r]] = {"type" : "Integer" ,
...
...
bench/ce/int_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/int.mlw T g_lab: Unknown (
other
)
bench/ce/int.mlw T g_lab: Unknown (
unknown
)
Counter-example model:File int.mlw:
Line 5:
x, [[@introduced], [@model_trace:x], [@model]] = {"type" : "Integer" ,
"val" : "48" }
bench/ce/int.mlw T g_no_lab: Unknown (
other
)
bench/ce/int.mlw T g_no_lab: Unknown (
unknown
)
Counter-example model:File int.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "48" }
bench/ce/int.mlw T g2_lab: Unknown (
other
)
bench/ce/int.mlw T g2_lab: Unknown (
unknown
)
Counter-example model:File int.mlw:
Line 9:
g, [[@model_trace:g]] = {"type" : "Integer" ,
...
...
@@ -19,7 +19,7 @@ Line 11:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/int.mlw T newgoal: Unknown (
other
)
bench/ce/int.mlw T newgoal: Unknown (
unknown
)
Counter-example model:File int.mlw:
Line 9:
g, [[@model_trace:g]] = {"type" : "Integer" ,
...
...
bench/ce/int_Z3,4.6.0.oracle
View file @
959aa08f
bench/ce/int.mlw T g_lab: Unknown (
other
)
bench/ce/int.mlw T g_lab: Unknown (
sat
)
Counter-example model:File int.mlw:
Line 5:
x, [[@introduced], [@model_trace:x], [@model]] = {"type" : "Integer" ,
"val" : "48" }
bench/ce/int.mlw T g_no_lab: Unknown (
other
)
bench/ce/int.mlw T g_no_lab: Unknown (
sat
)
Counter-example model:File int.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "48" }
bench/ce/int.mlw T g2_lab: Unknown (
other
)
bench/ce/int.mlw T g2_lab: Unknown (
sat
)
Counter-example model:File int.mlw:
Line 9:
g, [[@model_trace:g]] = {"type" : "Integer" ,
...
...
@@ -19,7 +19,7 @@ Line 11:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/int.mlw T newgoal: Unknown (
other
)
bench/ce/int.mlw T newgoal: Unknown (
sat
)
Counter-example model:File int.mlw:
Line 13:
X, [[@introduced], [@model], [@model_trace:X]] = {"type" : "Integer" ,
...
...
bench/ce/int_overflow_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/int_overflow.mlw ModelInt test0: Valid
bench/ce/int_overflow.mlw ModelInt test1: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test1: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 9:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/int_overflow.mlw ModelInt test2: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test2: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 14:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/int_overflow.mlw ModelInt test_overflow: Valid
bench/ce/int_overflow.mlw ModelInt test_overflow: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 18:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
@@ -21,7 +21,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/int_overflow.mlw ModelInt test_overflow2: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow2: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
@@ -29,7 +29,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
y, [[@introduced], [@model_trace:y]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/int_overflow.mlw ModelInt test_overflow2: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow2: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 23:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
@@ -38,7 +38,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int16: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow_int16: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 30:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
@@ -47,7 +47,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_alt: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_alt: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
@@ -56,7 +56,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_alt: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_alt: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 35:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
@@ -65,7 +65,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_bis: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow_int16_bis: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 40:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
@@ -74,7 +74,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "32768" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int32: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow_int32: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 48:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
@@ -83,7 +83,7 @@ y, [[@introduced],
[@model_trace:y]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int32_bis: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow_int32_bis: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 53:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
@@ -93,7 +93,7 @@ y, [[@introduced],
"val" : "1073741824" }
bench/ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline: Valid
bench/ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 58:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
bench/ce/int_overflow_Z3,4.6.0.oracle
View file @
959aa08f
bench/ce/int_overflow.mlw ModelInt test0: Valid
bench/ce/int_overflow.mlw ModelInt test1: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test1: Unknown (
sat
)
Counter-example model:File int_overflow.mlw:
Line 9:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/int_overflow.mlw ModelInt test2: Unknown (
other
)
bench/ce/int_overflow.mlw ModelInt test2: Unknown (
unknown
)
Counter-example model:File int_overflow.mlw:
Line 14:
x, [[@introduced], [@model_trace:x]] = {"type" : "Integer" ,
...
...
bench/ce/jlamp0_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/jlamp0.mlw M VC p1: Unknown (
other
)
bench/ce/jlamp0.mlw M VC p1: Unknown (
unknown
)
Counter-example model:File jlamp0.mlw:
Line 6:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
...
...
@@ -13,7 +13,7 @@ Line 12:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "3" }
bench/ce/jlamp0.mlw M VC p2: Unknown (
other
)
bench/ce/jlamp0.mlw M VC p2: Unknown (
unknown
)
Counter-example model:File jlamp0.mlw:
Line 6:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
...
...
@@ -26,7 +26,7 @@ c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "1" }
bench/ce/jlamp0.mlw M VC p2: Valid
bench/ce/jlamp0.mlw M VC p2: Unknown (
other
)
bench/ce/jlamp0.mlw M VC p2: Unknown (
unknown
)
Counter-example model:File jlamp0.mlw:
Line 6:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
...
...
@@ -48,7 +48,7 @@ Line 27:
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M VC p2: Unknown (
other
)
bench/ce/jlamp0.mlw M VC p2: Unknown (
unknown
)
Counter-example model:File jlamp0.mlw:
Line 6:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
...
...
@@ -71,7 +71,7 @@ Line 27:
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "12" }
bench/ce/jlamp0.mlw M VC p2: Unknown (
other
)
bench/ce/jlamp0.mlw M VC p2: Unknown (
unknown
)
Counter-example model:File jlamp0.mlw:
Line 6:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
...
...
@@ -94,7 +94,7 @@ Line 27:
c, [[@introduced], [@model_trace:c]] = {"type" : "Integer" ,
"val" : "4" }
bench/ce/jlamp0.mlw M VC p2: Unknown (
other
)
bench/ce/jlamp0.mlw M VC p2: Unknown (
unknown
)
Counter-example model:File jlamp0.mlw:
Line 6:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
...
...
bench/ce/jlamp_array_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/jlamp_array.mlw Array VC f: Unknown (
other
)
bench/ce/jlamp_array.mlw Array VC f: Unknown (
unknown
)
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
...
...
@@ -13,7 +13,7 @@ Line 22:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/jlamp_array.mlw Array VC f: Unknown (
other
)
bench/ce/jlamp_array.mlw Array VC f: Unknown (
unknown
)
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
...
...
@@ -34,7 +34,7 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/jlamp_array.mlw Array VC g: Valid
bench/ce/jlamp_array.mlw Array VC g: Unknown (
other
)
bench/ce/jlamp_array.mlw Array VC g: Unknown (
unknown
)
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
...
...
@@ -55,7 +55,7 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/jlamp_array.mlw Array VC h: Valid
bench/ce/jlamp_array.mlw Array VC h: Unknown (
other
)
bench/ce/jlamp_array.mlw Array VC h: Unknown (
unknown
)
Counter-example model:File jlamp_array.mlw:
Line 11:
two, [[@model_trace:two]] = {"type" : "Integer" ,
...
...
bench/ce/jlamp_projections_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/jlamp_projections.mlw Abstract VC p3: Valid
bench/ce/jlamp_projections.mlw Abstract VC p3: Unknown (
other
)
bench/ce/jlamp_projections.mlw Abstract VC p3: Unknown (
unknown
)
Counter-example model:File jlamp_projections.mlw:
Line 23:
a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
...
...
@@ -9,4 +9,4 @@ a, [[@introduced], [@model_trace:a]] = {"type" : "Integer" ,
"val" : "127" }
bench/ce/jlamp_projections.mlw Record VC p4: Valid
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (
other
)
bench/ce/jlamp_projections.mlw Record VC p4: Unknown (
unknown
)
bench/ce/list_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/list.mlw List_int g1: Unknown (
other
)
bench/ce/list.mlw List_int g2: Unknown (
other
)
bench/ce/list.mlw List_poly g1: Unknown (
other
)
bench/ce/list.mlw List_poly g2: Unknown (
other
)
bench/ce/list.mlw List_int g1: Unknown (
unknown
)
bench/ce/list.mlw List_int g2: Unknown (
unknown
)
bench/ce/list.mlw List_poly g1: Unknown (
unknown
)
bench/ce/list.mlw List_poly g2: Unknown (
unknown
)
bench/ce/map_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/map.mlw ModelMap t1: Unknown (
other
)
bench/ce/map.mlw ModelMap t1: Unknown (
sat
)
Counter-example model:File map.mlw:
Line 5:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
@@ -8,7 +8,7 @@ t, [[@introduced], [@model_trace:t]] = {"type" : "Array" ,
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/map.mlw M VC test_map: Unknown (
other
)
bench/ce/map.mlw M VC test_map: Unknown (
unknown
)
Counter-example model:File map.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
...
...
@@ -28,7 +28,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/map.mlw M VC test_map_multidim1: Unknown (
other
)
bench/ce/map.mlw M VC test_map_multidim1: Unknown (
unknown
)
Counter-example model:File map.mlw:
Line 22:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
...
...
@@ -46,7 +46,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
bench/ce/map.mlw M VC test_map_multidim2: Unknown (
other
)
bench/ce/map.mlw M VC test_map_multidim2: Unknown (
unknown
)
Counter-example model:File map.mlw:
Line 27:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
...
...
@@ -76,7 +76,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
{"others" : {"type" : "Array" , "val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] } }] }
bench/ce/map.mlw M VC proj_map_test1: Unknown (
other
)
bench/ce/map.mlw M VC proj_map_test1: Unknown (
unknown
)
Counter-example model:File map.mlw:
Line 34:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
...
...
@@ -96,7 +96,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
bench/ce/map.mlw M VC proj_map_test2: Unknown (
other
)
bench/ce/map.mlw M VC proj_map_test2: Unknown (
unknown
)
Counter-example model:File map.mlw:
Line 39:
x, [[@introduced], [@model_trace:x]] = {"type" : "Array" ,
...
...
bench/ce/map_Z3,4.6.0.oracle
View file @
959aa08f
bench/ce/map.mlw ModelMap t1: Unknown (
other
)
bench/ce/map.mlw ModelMap t1: Unknown (
sat
)
Counter-example model:File map.mlw:
Line 5:
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
...
...
bench/ce/real_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/real.mlw ModelReal test1: Unknown (
other
)
bench/ce/real.mlw ModelReal test1: Unknown (
unknown
)
Counter-example model:File real.mlw:
Line 5:
x, [[@introduced], [@model_trace:x]] = {"type" : "Fraction" ,
"val" : "1\/4" }
bench/ce/real.mlw ModelReal test2: Unknown (
other
)
bench/ce/real.mlw ModelReal test2: Unknown (
unknown
)
Counter-example model:File real.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Decimal" ,
...
...
bench/ce/real_Z3,4.6.0.oracle
View file @
959aa08f
bench/ce/real.mlw ModelReal test1: Unknown (
other
)
bench/ce/real.mlw ModelReal test1: Unknown (
sat
)
Counter-example model:File real.mlw:
Line 5:
x, [[@introduced], [@model_trace:x]] = {"type" : "Fraction" ,
"val" : "1\/2" }
bench/ce/real.mlw ModelReal test2: Unknown (
other
)
bench/ce/real.mlw ModelReal test2: Unknown (
sat
)
Counter-example model:File real.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Decimal" ,
...
...
bench/ce/record_map_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/record_map.mlw M VC map_record_proj_test1: Unknown (
other
)
bench/ce/record_map.mlw M VC map_record_proj_test1: Unknown (
unknown
)
Counter-example model:File record_map.mlw:
Line 41:
map_rec, [[@model_projected], [@introduced],
...
...
@@ -21,7 +21,7 @@ map_rec, [[@model_projected], [@introduced],
"value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
bench/ce/record_map.mlw M VC record_map_proj_test2: Unknown (
other
)
bench/ce/record_map.mlw M VC record_map_proj_test2: Unknown (
unknown
)
Counter-example model:File record_map.mlw:
Line 46:
rec_map, [[@model_projected], [@introduced],
...
...
@@ -56,7 +56,7 @@ rec_map.g_map, [[@model_projected], [@introduced],
[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
"val" : false }
bench/ce/record_map.mlw M VC record_map_proj_test3: Unknown (
other
)
bench/ce/record_map.mlw M VC record_map_proj_test3: Unknown (
unknown
)
Counter-example model:File record_map.mlw:
Line 51:
re_rec_map, [[@model_projected], [@introduced],
...
...
bench/ce/record_map_Z3,4.6.0.oracle
View file @
959aa08f
bench/ce/record_map.mlw M VC map_record_proj_test1: Unknown (
other
)
bench/ce/record_map.mlw M VC map_record_proj_test1: Unknown (
sat
)
Counter-example model:File record_map.mlw:
Line 41:
map_rec, [[@model_projected], [@introduced],
...
...
@@ -15,7 +15,7 @@ map_rec, [[@model_projected], [@introduced],
"val" : "1" } }, {"field" : "g" , "value" : {"type" : "Boolean" ,
"val" : false } }] } } }] }
bench/ce/record_map.mlw M VC record_map_proj_test2: Unknown (
other
)
bench/ce/record_map.mlw M VC record_map_proj_test2: Unknown (
sat
)
Counter-example model:File record_map.mlw:
Line 46:
rec_map, [[@model_projected], [@introduced],
...
...
@@ -46,7 +46,7 @@ rec_map.g_map, [[@model_projected], [@introduced],
[@model_trace:rec_map.g_map]] = {"type" : "Boolean" ,
"val" : false }
bench/ce/record_map.mlw M VC record_map_proj_test3: Unknown (
other
)
bench/ce/record_map.mlw M VC record_map_proj_test3: Unknown (
sat
)
Counter-example model:File record_map.mlw:
Line 51:
re_rec_map, [[@model_projected], [@introduced],
...
...
bench/ce/records_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/records.mlw M VC record_match_eval_test1: Unknown (
other
)
bench/ce/records.mlw M VC record_match_eval_test1: Unknown (
unknown
)
bench/ce/records.mlw M VC record_match_eval_test1: Valid
bench/ce/records.mlw M VC record_match_eval_test2: Unknown (
other
)
bench/ce/records.mlw M VC record_match_eval_test3: Unknown (
other
)
bench/ce/records.mlw M VC record_match_eval_test4: Unknown (
other
)
bench/ce/records.mlw M VC test_record_match_eval_test5: Unknown (
other
)
bench/ce/records.mlw Mutable VC record_match_eval_test1: Unknown (
other
)
bench/ce/records.mlw M VC record_match_eval_test2: Unknown (
unknown
)
bench/ce/records.mlw M VC record_match_eval_test3: Unknown (
unknown
)
bench/ce/records.mlw M VC record_match_eval_test4: Unknown (
unknown
)
bench/ce/records.mlw M VC test_record_match_eval_test5: Unknown (
unknown
)
bench/ce/records.mlw Mutable VC record_match_eval_test1: Unknown (
unknown
)
Counter-example model:File records.mlw:
Line 57:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
...
...
@@ -20,7 +20,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : true } }] } }
bench/ce/records.mlw Mutable VC record_match_eval_test1: Valid
bench/ce/records.mlw Mutable VC record_match_eval_test2: Unknown (
other
)
bench/ce/records.mlw Mutable VC record_match_eval_test2: Unknown (
unknown
)
Counter-example model:File records.mlw:
Line 65:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
...
...
@@ -35,7 +35,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw Mutable VC record_match_eval_test3: Unknown (
other
)
bench/ce/records.mlw Mutable VC record_match_eval_test3: Unknown (
unknown
)
Counter-example model:File records.mlw:
Line 70:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
...
...
@@ -56,7 +56,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw Mutable VC record_match_eval_test4: Unknown (
other
)
bench/ce/records.mlw Mutable VC record_match_eval_test4: Unknown (
unknown
)
Counter-example model:File records.mlw:
Line 75:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
...
...
bench/ce/records_Z3,4.6.0.oracle
View file @
959aa08f
...
...
@@ -4,7 +4,7 @@ bench/ce/records.mlw M VC record_match_eval_test2: Timeout
bench/ce/records.mlw M VC record_match_eval_test3: Timeout
bench/ce/records.mlw M VC record_match_eval_test4: Timeout
bench/ce/records.mlw M VC test_record_match_eval_test5: Timeout
bench/ce/records.mlw Mutable VC record_match_eval_test1: Unknown (
other
)
bench/ce/records.mlw Mutable VC record_match_eval_test1: Unknown (
sat
)
Counter-example model:File records.mlw:
Line 57:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
...
...
@@ -20,7 +20,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"val" : true } }] } }
bench/ce/records.mlw Mutable VC record_match_eval_test1: Valid
bench/ce/records.mlw Mutable VC record_match_eval_test2: Unknown (
other
)
bench/ce/records.mlw Mutable VC record_match_eval_test2: Unknown (
sat
)
Counter-example model:File records.mlw:
Line 65:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
...
...
@@ -35,7 +35,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw Mutable VC record_match_eval_test3: Unknown (
other
)
bench/ce/records.mlw Mutable VC record_match_eval_test3: Unknown (
sat
)
Counter-example model:File records.mlw:
Line 70:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
...
...
@@ -56,7 +56,7 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
"value" : {"type" : "Boolean" ,
"val" : false } }] } }
bench/ce/records.mlw Mutable VC record_match_eval_test4: Unknown (
other
)
bench/ce/records.mlw Mutable VC record_match_eval_test4: Unknown (
sat
)
Counter-example model:File records.mlw:
Line 75:
x, [[@introduced], [@model_trace:x]] = {"type" : "Record" ,
...
...
bench/ce/ref_CVC4,1.5.oracle
View file @
959aa08f
bench/ce/ref.mlw M VC test_post: Unknown (
other
)
bench/ce/ref.mlw M VC test_post: Unknown (
unknown
)
Counter-example model:File ref.mlw: