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
125
Issues
125
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
a67650db
Commit
a67650db
authored
Jul 11, 2018
by
Sylvain Dailler
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Remove label model which is redundant with model_trace label.
#108
parent
6fae2d4a
Changes
40
Hide whitespace changes
Inline
Side-by-side
Showing
40 changed files
with
596 additions
and
597 deletions
+596
-597
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
+28
-28
bench/ce/array_records_Z3,4.6.0.oracle
bench/ce/array_records_Z3,4.6.0.oracle
+28
-28
bench/ce/floats_CVC4,1.5.oracle
bench/ce/floats_CVC4,1.5.oracle
+20
-20
bench/ce/floats_Z3,4.6.0.oracle
bench/ce/floats_Z3,4.6.0.oracle
+40
-40
bench/ce/if_decision_branch_CVC4,1.5.oracle
bench/ce/if_decision_branch_CVC4,1.5.oracle
+3
-3
bench/ce/if_decision_branch_Z3,4.6.0.oracle
bench/ce/if_decision_branch_Z3,4.6.0.oracle
+3
-3
bench/ce/int32_CVC4,1.5.oracle
bench/ce/int32_CVC4,1.5.oracle
+4
-4
bench/ce/int32_Z3,4.6.0.oracle
bench/ce/int32_Z3,4.6.0.oracle
+4
-4
bench/ce/int_CVC4,1.5.oracle
bench/ce/int_CVC4,1.5.oracle
+16
-20
bench/ce/int_Z3,4.6.0.oracle
bench/ce/int_Z3,4.6.0.oracle
+15
-19
bench/ce/int_overflow_CVC4,1.5.oracle
bench/ce/int_overflow_CVC4,1.5.oracle
+22
-23
bench/ce/int_overflow_Z3,4.6.0.oracle
bench/ce/int_overflow_Z3,4.6.0.oracle
+22
-25
bench/ce/jlamp0_CVC4,1.5.oracle
bench/ce/jlamp0_CVC4,1.5.oracle
+36
-38
bench/ce/jlamp0_Z3,4.6.0.oracle
bench/ce/jlamp0_Z3,4.6.0.oracle
+36
-38
bench/ce/jlamp_array_CVC4,1.5.oracle
bench/ce/jlamp_array_CVC4,1.5.oracle
+22
-22
bench/ce/jlamp_array_Z3,4.6.0.oracle
bench/ce/jlamp_array_Z3,4.6.0.oracle
+11
-11
bench/ce/jlamp_projections_CVC4,1.5.oracle
bench/ce/jlamp_projections_CVC4,1.5.oracle
+2
-2
bench/ce/jlamp_projections_Z3,4.6.0.oracle
bench/ce/jlamp_projections_Z3,4.6.0.oracle
+2
-2
bench/ce/map_CVC4,1.5.oracle
bench/ce/map_CVC4,1.5.oracle
+30
-25
bench/ce/map_Z3,4.6.0.oracle
bench/ce/map_Z3,4.6.0.oracle
+30
-25
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
+32
-32
bench/ce/record_map_Z3,4.6.0.oracle
bench/ce/record_map_Z3,4.6.0.oracle
+32
-32
bench/ce/records_CVC4,1.5.oracle
bench/ce/records_CVC4,1.5.oracle
+22
-16
bench/ce/records_Z3,4.6.0.oracle
bench/ce/records_Z3,4.6.0.oracle
+22
-16
bench/ce/ref_CVC4,1.5.oracle
bench/ce/ref_CVC4,1.5.oracle
+36
-37
bench/ce/ref_Z3,4.6.0.oracle
bench/ce/ref_Z3,4.6.0.oracle
+37
-37
bench/ce/result_CVC4,1.5.oracle
bench/ce/result_CVC4,1.5.oracle
+8
-8
bench/ce/result_Z3,4.6.0.oracle
bench/ce/result_Z3,4.6.0.oracle
+8
-8
bench/ce/simple_array_CVC4,1.5.oracle
bench/ce/simple_array_CVC4,1.5.oracle
+3
-4
bench/ce/simple_array_Z3,4.6.0.oracle
bench/ce/simple_array_Z3,4.6.0.oracle
+3
-4
src/core/ident.ml
src/core/ident.ml
+5
-6
src/core/ident.mli
src/core/ident.mli
+0
-1
src/parser/parser.mly
src/parser/parser.mly
+1
-1
src/printer/alt_ergo.ml
src/printer/alt_ergo.ml
+3
-3
src/printer/smtv2.ml
src/printer/smtv2.ml
+3
-4
src/transform/intro_projections_counterexmp.ml
src/transform/intro_projections_counterexmp.ml
+1
-2
No files found.
bench/ce/algebraic_type_CVC4,1.5.oracle
View file @
a67650db
bench/ce/algebraic_type.mlw M G: Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Apply" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type_Z3,4.6.0.oracle
View file @
a67650db
bench/ce/algebraic_type.mlw M G: Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 6:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Apply" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/array_records_CVC4,1.5.oracle
View file @
a67650db
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
Line 31:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Unknown (other)
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
Line 25:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "0" }
bench/ce/array_records_Z3,4.6.0.oracle
View file @
a67650db
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 27:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 28:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 29:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
Line 30:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
Line 31:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/array_records.mlw Array_records VC var_overwrite: Timeout
Counter-example model:File array_records.mlw:
Line 23:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
Line 25:
i, [[@
model], [@
introduced], [@model_trace:i]] = {"type" : "Integer" ,
i, [[@introduced], [@model_trace:i]] = {"type" : "Integer" ,
"val" : "2" }
bench/ce/floats_CVC4,1.5.oracle
View file @
a67650db
bench/ce/floats.mlw T32 g1: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g2: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g3: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g5: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g6: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g7: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g8: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T32 g10: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g1: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g2: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g3: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g5: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g6: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g7: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g8: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats.mlw T64 g10: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "-1" }
bench/ce/floats_Z3,4.6.0.oracle
View file @
a67650db
bench/ce/floats.mlw T32 g1: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 5:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 7:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 9:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T32 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 11:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 13:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 15:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Not_a_number" } }
bench/ce/floats.mlw T32 g7: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 17:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 19:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Plus_infinity" } }
bench/ce/floats.mlw T32 g9: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 21:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 23:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 31:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
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
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 33:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "-0x0.0000040000000p-1023" ,
"value" : -2.65249e-315 } }
bench/ce/floats.mlw T64 g3: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 35:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Minus_zero" } }
bench/ce/floats.mlw T64 g4: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 37:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.4000000000000p0" ,
"value" : 1.25 } }
bench/ce/floats.mlw T64 g5: Timeout
Counter-example model:File ieee_float.mlw:
Line 218:
max_int, [[@model
], [@model
_trace:max_int]] = {"type" : "Integer" ,
max_int, [[@model_trace:max_int]] = {"type" : "Integer" ,
"val" : "5" }
File floats.mlw:
Line 39:
x, [[@
model], [@
introduced], [@model_trace:x]] = {"type" : "Float" ,
x, [[@introduced], [@model_trace:x]] = {"type" : "Float" ,
"val" : {"cons" : "Float_hexa" , "str_hexa" : "0x1.0000000000001p51