ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/bench/check-ce
History
Claude Marche 116c0aa789 There is no symbol ae.sqrt_real parsed by Alt-Ergo 2.6
2025-06-13 08:23:33 +02:00
..
oracles
There is no symbol ae.sqrt_real parsed by Alt-Ergo 2.6
2025-06-13 08:23:33 +02:00
petiot2018
do not map IEEE floats theory to Alt-Ergo's own theory
2025-05-22 19:49:00 +02:00
614.mlw
Resolve "Rac checker returns incorrect result with expl attr"
2022-02-18 11:24:51 +00:00
615.mlw
Resolve "Rac checker returns incorrect result with expl attr"
2022-02-18 11:24:51 +00:00
640_no_loc_failure.mlw
(Check_ce] RAC should also execute goals
2022-09-26 14:57:32 +02:00
657.mlw
Generate return value in models for val functions
2022-06-21 12:02:01 +02:00
668_projection.mlw
[import_model_value] Check type while filtering lsymbols for projections
2022-07-28 10:24:52 +00:00
703_reduce_term.mlw
Attach a unique identifier to each mlw expression
2023-07-07 17:41:09 +00:00
algebraic_types_mono.mlw
Move algebraic_types_mono, recursive_model and simple_array from ce to check-ce bench
2022-09-28 16:45:21 +02:00
algebraic_types_poly.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
anonymous1.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
anonymous2.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
anonymous3.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
anonymous4.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
anonymous5.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
anonymous6_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
anonymous6.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
array_mono.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
array_poly.mlw
Catch uncaught exceptions in RAC and return Incomplete / Move check-ce-xfail to check-ce
2022-11-28 13:30:34 +01:00
array_records_mono.mlw
Add monomorphic versions for tests with polymorphism in CE bench
2022-10-26 18:05:44 +02:00
array_records_poly.mlw
Resolve "using model_projection on alias types should be forbidden"
2024-04-16 19:56:53 +02:00
attributes_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
attributes.mlw
(CE bench) Moving attributes.mlw test to check-ce
2022-08-22 15:55:58 +02:00
blackbox.mlw
Support for CVC5
2022-06-03 16:30:54 +00:00
bv32_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
bv32_toBig.mlw
(CE bench) Update comment
2022-08-22 15:55:58 +02:00
bv32.mlw
Generate return value in models for val functions
2022-06-21 12:02:01 +02:00
call-val-function.mlw
(CE bench) Cleanup duplicated module in check-ce/call-val-function
2022-08-22 15:58:14 +02:00
division_by_zero.mlw
RAC: Add new exception for cases where context is available
2024-09-20 08:41:30 +02:00
double_projection.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
falseCE.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
fide21.mlw
Generate return value in models for val functions
2022-06-21 12:02:01 +02:00
float_div.mlw
Do not introduce program variables for zero and one in int.Int module
2025-03-26 15:17:05 +01:00
floats.mlw
Update oracle for floats.mlw
2023-02-01 12:30:37 +01:00
for1_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
for1.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
for_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
for.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
func_call1_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
func_call1.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
func_call2.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
func_call3.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
func_call4_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
func_call4.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
func_call5_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
func_call5.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
func_call6_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
func_call6.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
func_call_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
func_call.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
global_logic_constant.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
if_assign.mlw
(CE bench) Move if_assign, int32, loop_ce, loop_inv, range_type to check-ce
2022-08-22 15:55:58 +02:00
if_decision_branch.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
int32_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
int32.mlw
(CE bench) Move if_assign, int32, loop_ce, loop_inv, range_type to check-ce
2022-08-22 15:55:58 +02:00
int_overflow.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
integers.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
j3_1.mlw
Do not introduce program variables for zero and one in int.Int module
2025-03-26 15:17:05 +01:00
jlamp0_mono.mlw
Fix CE oracles and add a new example
2021-09-24 16:40:01 +02:00
jlamp0_poly.mlw
Add monomorphic versions for tests with polymorphism in CE bench
2022-10-26 18:05:44 +02:00
jlamp_array_mono.mlw
Add monomorphic versions for tests with polymorphism in CE bench
2022-10-26 18:05:44 +02:00
jlamp_array_poly.mlw
Add monomorphic versions for tests with polymorphism in CE bench
2022-10-26 18:05:44 +02:00
jlamp_projections.mlw
(CE bench) Move jlamp_projections from ce to check-ce bench
2022-08-22 15:55:58 +02:00
let_constant.mlw
(CE bench) Move let_constant and result from ce to check-ce bench
2022-08-22 15:55:58 +02:00
let_function_logic.mlw
Update oracle files / Add new tests in check-ce bench
2023-02-13 14:47:35 +01:00
let_function.mlw
Update oracle files / Add new tests in check-ce bench
2023-02-13 14:47:35 +01:00
lists.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
log-asserts.mlw
Add CE examples from Decysif
2024-10-21 15:09:43 +02:00
log-call-nc.mlw
Add CE examples from Decysif
2024-10-21 15:09:43 +02:00
log-cond.mlw
Add CE examples from Decysif
2024-10-21 15:09:43 +02:00
log-logic.mlw
Add CE examples from Decysif
2024-10-21 15:09:43 +02:00
log-post.mlw
Add CE examples from Decysif
2024-10-21 15:09:43 +02:00
log-simple.mlw
Add CE examples from Decysif
2024-10-21 15:09:43 +02:00
logic_constant.mlw
Update oracle files / Add new tests in check-ce bench
2023-02-13 14:47:35 +01:00
logic_function.mlw
Update oracle files / Add new tests in check-ce bench
2023-02-13 14:47:35 +01:00
loop_ce_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
loop_ce.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
loop_inv_int_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
loop_inv_int.mlw
(CE bench) Move if_assign, int32, loop_ce, loop_inv, range_type to check-ce
2022-08-22 15:55:58 +02:00
loop_inv_real_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
loop_inv_real.mlw
Catch uncaught exceptions in RAC and return Incomplete / Move check-ce-xfail to check-ce
2022-11-28 13:30:34 +01:00
manual_map.mlw
doc
2023-02-06 10:37:02 +01:00
map_of_algebraic.mlw
smtv2-model-parser: improve conversion from sort to ty
2023-04-25 09:21:34 +02:00
maps_mono.mlw
Add monomorphic versions for tests with polymorphism in CE bench
2022-10-26 18:05:44 +02:00
maps_poly.mlw
Add monomorphic versions for tests with polymorphism in CE bench
2022-10-26 18:05:44 +02:00
model_projection2.mlw
check-ce script does run petiot when file is given.
2024-02-20 10:55:19 +01:00
model_projection3.mlw
Disable completely prepare_for_counterexamples
2024-10-11 13:30:51 +02:00
model_projection.mlw
Disable all usage of meta model_projected
2024-01-17 03:43:15 +00:00
multifile1.mlw
rename check-ce example
2020-10-05 09:46:45 +02:00
multifile2.mlw
(CE bench) Minor comments update
2022-08-22 15:55:58 +02:00
polymorphism.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
range_type_float.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
range_type_int.mlw
(CE bench) Move if_assign, int32, loop_ce, loop_inv, range_type to check-ce
2022-08-22 15:55:58 +02:00
real_values.mlw
Update some oracles after checking the diffs
2023-02-01 12:30:37 +01:00
record_map.mlw
(CE bench) Move record_map, record_nested_one_field, records_inv, records_label to check-ce
2022-08-22 15:57:38 +02:00
record_nested_one_field.mlw
(CE bench) Move record_map, record_nested_one_field, records_inv, records_label to check-ce
2022-08-22 15:57:38 +02:00
records_inv.mlw
(CE bench) Move record_map, record_nested_one_field, records_inv, records_label to check-ce
2022-08-22 15:57:38 +02:00
records_label.mlw
(CE bench) Move record_map, record_nested_one_field, records_inv, records_label to check-ce
2022-08-22 15:57:38 +02:00
recursive_model.mlw
Move algebraic_types_mono, recursive_model and simple_array from ce to check-ce bench
2022-09-28 16:45:21 +02:00
ref1_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
ref1.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
ref2_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
ref2.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
ref_ex_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
ref_ex.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
ref_mono.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
result.mlw
(CE bench) Move let_constant and result from ce to check-ce bench
2022-08-22 15:55:58 +02:00
return_value_below_if_when_vc_sp.mlw
introduce_premises also "dequant" the let-ins
2022-04-21 16:23:20 +00:00
simple_array.mlw
Move algebraic_types_mono, recursive_model and simple_array from ce to check-ce bench
2022-09-28 16:45:21 +02:00
strings.mlw
Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail
2022-10-20 16:39:10 +02:00
test_result_ce_value0.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
test_result_ce_value1.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
test_result_ce_value2.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
threshold.mlw
(CE bench) Move threshold.mlw to check-ce
2022-08-22 15:58:14 +02:00
tuple1.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
tuple.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
underspec_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
underspec.mlw
(CE bench) Minor comments update
2022-08-22 15:55:58 +02:00
val_function.mlw
Update oracle files / Add new tests in check-ce bench
2023-02-13 14:47:35 +01:00
var_clones.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
while1_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
while1.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00
while_mono.mlw
update CE oracles
2023-02-01 10:39:08 +01:00
while.mlw
fix check-ce-bench
2021-07-12 12:21:57 +02:00