Skip to content

SMT: Handle fixed-width integers in counterexamples #649

SMT: Handle fixed-width integers in counterexamples

SMT: Handle fixed-width integers in counterexamples #649

GitHub Actions / Test Results succeeded Mar 1, 2024 in 0s

All 612 tests pass in 0s

    9 files  ±0     20 suites  ±0   0s ⏱️ ±0s
  612 tests ±0    612 ✅ ±0  0 💤 ±0  0 ❌ ±0 
1 969 runs  ±0  1 968 ✅ ±0  1 💤 ±0  0 ❌ ±0 

Results for commit 87ce5f2. ± Comparison against earlier commit a05525a.

Annotations

Check notice on line 0 in .github

See this annotation in the file changed.

@github-actions github-actions / Test Results

612 tests found

There are 612 tests, see "Raw output" for the full list of tests.
Raw output
Replicate.sail
abstract_bool.sail
abstract_bool2.sail
abstract_bool_inconsistent.sail
add_overflow.sat.sail
add_overflow.unsat.sail
add_real.sail
add_vec_exts_no_annot.sail
add_vec_exts_no_annot_overload.sail
add_vec_lit.sail
add_vec_lit_old.sail
all_even_vector_length.sail
allpats.sail
and_block.sail
and_let_bool.sail
anf_as_pattern.sail
anf_block.sail
anon_rec.sail
arith_C128FL.unsat.sail
arith_C64C32CB.unsat.sail
arith_FFL_1.unsat.sail
arith_FFL_2.unsat.sail
arith_FFL_3.unsat.sail
arith_FFL_4.unsat.sail
arith_FFL_5.unsat.sail
arith_LC32L.unsat.sail
arith_LC32L_1.unsat.sail
arith_LC32L_2.unsat.sail
arith_LC32L_3.unsat.sail
arith_LC32L_4.unsat.sail
arith_LCBL.unsat.sail
arm_FPEXC1.sail
arm_types.sail
as_pattern.sail
assign_rename_bug.sail
assignment_simple.sail
atomcase.sail
bad_option_pragma.sail
bad_option_pragma2.sail
basic_1.sat.sail
basic_1.unsat.sail
basic_2.sat.sail
basic_2.unsat.sail
bind_typ_var.sail
bitfield_abs.sail
bitfield_error.sail
bitfield_exponential.sail
bitfield_mod.sail
bitfield_pc.sail
bitfield_updates.sail
bitfield_updates0.sail
bits_concat_pattern.sail
bitvector.sail
bitvector_param.sail
bitvector_update.sail
bitvector_update2.sail
bitwise_not.sail
bitwise_not_gen.sail
bitwise_not_x3.sail
block.sail
bool_bits_mapping.sail
bool_constraint.sail
bool_typ_pat.sail
built bitfield/
built for_bounds/
built hello_world/
built is_x_subrange/
built loop/
built lsl/
built new_bitfields/
built pattern1/
built pure_rebind/
built reg_alias/
built reg_passing/
built reg_ref/
built short_circuit/
built string_equality/
built string_of_struct/
built trycatch/
built types/
built vec_32_64/
built void/
bv_literal.sail
bv_simple_index_bit.sail
bv_update_error.sail
can_hang.sail
case_simple1.sail
case_simple2.sail
cast_lexp1.sail
cast_lexp2.sail
cast_simple.sail
ccheri_regression1.unsat.sail
cfold_reg.sail
cheri128_hsb.sail
cheri_capreg.sail
cheri_capstruct_order.sail
clear_overflow_regression.unsat.sail
commentfix.sail
complete_pattern_let.sail
complex_exist_sat.sail
concat_prop.unsat.sail
concat_prop128.unsat.sail
concurrency_interface.sail
concurrency_interface_dec.sail
concurrency_interface_inc.sail
cond_mod.sail
config.sail
config_register.sail
cons_pattern.sail
cons_pattern_synonym.sail
cons_wildcard_insert.sail
constrained_function.sail
constrained_function_scattered.sail
constrained_struct.sail
constraint_ctor.sail
constraint_syn.sail
constructor247.sail
cr_invisible.sail
crlf.sail
custom_flow.sail
dead_branch.sail
dec_prelude.sail
decode_patterns.sail
default_order.sail
deinfix_plus.sail
doc_comment_eof.sail
double_option.sail
downcast_fn.sail
duplicate_binding.sail
duplicate_builtin.sail
duplicate_ctor.sail
duplicate_quant.sail
duplicate_toplevel_let.sail
duplicate_toplevel_let_mod.sail
duplicate_type_id.sail
duplicate_type_id2.sail
duplicate_type_id3.sail
duplicate_type_id4.sail
duplicate_type_id5.sail
duplicate_type_id6.sail
either.sail
either_rvbug.sail
empty_list.sail
empty_su.sail
empty_vector_infer.sail
encdec.sail
encdec.sat.sail
enum_cast.sail
enum_map.sail
enum_match.sail
enum_tup_match.sail
eq_struct.sail
eqn_inst.sail
equation_arguments.sail
equation_return.sail
ex_cast.sail
exception.unsat.sail
exception_2.unsat.sail
exception_3.unsat.sail
execute_decode_hard.sail
exint.sail
exist1.sail
exist2.sail
exist_simple.sail
exist_subrange.sail
exist_synonym.sail
exist_tlb.sail
exist_true.sail
existential_ast.sail
existential_ast2.sail
existential_ast3.sail
existential_constraint_synonym.sail
exit1.sail
exit2.sail
exit3.sail
extend_simple.sail
extended_ascii.sail
extension_constructor.sail
fail_assert_mono_bug.sail
fail_exception.sail
fail_issue203.sail
fallthrough_exception.sail
fast_signed.sail
floor_pow2.sail
flow_gt1.sail
flow_gteq1.sail
flow_lt1.sail
flow_lt2.sail
flow_lteq1.sail
flow_restrict.sail
for_shadow.sail
foreach_e.sail
foreach_none.sail
foreach_simple.unsat.sail
foreach_simple_2.unsat.sail
foreach_var_updates.sail
fpthreesimp.sail
funcl_guard.sail
function_namespace.sail
function_quant.sail
fvector_update.sail
get_slice_int.sail
global_false_constraint.sail
global_let_shadow.sail
global_type_var.sail
guards.sail
gvector.sail
gvector.unsat.sail
gvector_trivial.unsat.sail
gvectorlit.sail
help_option_pragma.sail
if_infer.sail
if_opt_typ.sail
if_return.sail
if_var_updates.sail
illegal_escape.sail
implicits.sail
import_reserved.sail
inc_prelude.sail
inc_tests.sail
infix_include.sail
inline_regression.unsat.sail
inline_test_1.unsat.sail
inline_typ.sail
int64_vector_literal.sail
int_pattern.sail
int_struct.sail
int_struct_constrained.sail
int_synonym.sail
invalid_function_val.sail
issue136.sail
issue202_1.sail
issue232.sail
issue232_2.sail
issue243.sail
issue243_fixed.sail
issue244_1.sail
issue244_2.sail
issue244_3.sail
issue244_4.sail
issue250.sail
issue277.sail
issue362.sail
issue37.sail
issue401.sail
issue429.sail
issue434.sail
large_bitvector.sail
let_intervene.unsat.sail
let_option.sail
let_subtyp_bug.sail
letbind.sail
lexp_vec.sail
lib_hex_bits.sail
line_comment_eof.sail
list_cons.sail
list_cons2.sail
list_cons_cons.sail
list_let.sail
list_lit.sail
list_mut.sail
list_rec_functions1.sail
list_rec_functions2.sail
list_scope.sail
list_scope2.sail
list_scope3.sail
list_test.sail
list_torture.sail
load_store_dep.sat.sail
lookup.sail
loop_exception.sail
lt_flow.sail
lt_int_irrefl.unsat.sail
lt_int_trans.unsat.sail
lteq_int_antisym.unsat.sail
lteq_int_def.unsat.sail
lteq_int_refl.unsat.sail
lteq_int_trans.unsat.sail
lzcnt.unsat.sail
lzcnt_2.unsat.sail
lzcnt_3.unsat.sail
mapping.sail
mapping_body_private.sail
mapping_clause.sail
mapping_compose.sail
mapping_rreg.sail
mapping_two_type.sail
match_bind.sail
match_fail.sat.sail
match_fail_query_1.sat.sail
match_fail_query_2.sat.sail
mem_builtins.unsat.sail
minmax.unsat.sail
minmax_1.sat.sail
minmax_2.sat.sail
missing_tick.sail
mix_declaration_update.sail
mod_var.sail
modify_assignment1.sail
modify_enum.sail
modify_enum2.sail
modify_immutable.sail
modify_immutable2.sail
modify_type_chain.sail
module_reserved.sail
multiple_unifiers.sail
mutrec.sail
nat_set.sail
negative_bits_existential.sail
negative_bits_list.sail
negative_bits_struct.sail
negative_bits_struct2.sail
negative_bits_tuple.sail
negative_bits_union.sail
negative_bits_union2.sail
nested_fields.sail
nested_mapping.sail
new_bitfields.sail
nexp_simp_euclidian.sail
nexp_synonym.sail
nexp_synonym2.sail
nlflow.sail
no_function.sail
no_function2.sail
no_function3.sail
no_val_recur.sail
non_synonym.sail
non_unique.sail
nonexistent_overload.sail
nonexistent_pragma.sail
not_pattern.sail
nzcv.sail
option.sail
option_either.sail
option_nest.sail
option_option.sail
option_tuple.sail
order.unsat.sail
outcome_impl.sail
outcome_impl_quant.sail
overlap_field.sail
overload_bound.sail
overload_mapping.sail
overload_member_scope.sail
overload_overload.sail
overload_plus.sail
pat_completeness.sail
pattern_concat_nest.sail
patternrefinement.sail
patterns.sail
pc_no_wildcard.sail
phantom_bitlist_struct.sail
phantom_bitlist_union.sail
phantom_num.sail
phantom_option.sail
plus_one_unify.sail
pointer_assign.sail
poly_int_record.sail
poly_list.sail
poly_mapping.sail
poly_mapping2.sail
poly_outcome.sail
poly_pair.sail
poly_record.sail
poly_simple.sail
poly_tup.sail
poly_union.sail
poly_union_rev.sail
poly_vector.sail
pow2.sail
pow_32_64.sail
pow_unify.sail
pr194.sail
pragma_block.sail
prelude.sail
prelude_no_order.sail
primop.sail
priv_fn_no_val.sail
private_clause.sail
private_ctor.sail
private_extension.sail
private_function.sail
private_scattered_enum.sail
private_scattered_fn.sail
private_scattered_map.sail
private_scattered_union.sail
private_union.sail
procstate1.sail
pub_val_priv_fn.sail
pure_let_var.sail
pure_let_var2.sail
pure_record.sail
pure_record2.sail
pure_record3.sail
range.sail
read_write_ram.sail
real.sail
real.unsat.sail
real_prop.sail
recursion.sail
reg_32_64.sail
reg_init_let.sail
reg_list.sail
reg_mod.sail
reg_option.sail
reg_ref.sail
reg_ref.unsat.sail
reg_ref_nb.sail
repeat_constraint.sail
return_leak.sail
return_register_ref.sail
return_simple1.sail
return_simple2.sail
return_simple3.sail
return_simple4.sail
revrev_endianness.unsat.sail
rmem_rmemt_same.sail
rv_add_0.sat.sail
rv_add_0.unsat.sail
rv_add_1.sat.sail
rv_add_1.unsat.sail
rv_add_decode.unsat.sail
rv_duopod_bug.sail
rv_format.sail
rv_format2.sail
rv_memop.sail
rv_reg_rw.unsat.sail
sail_mask.unsat.sail
sail_mask_2.unsat.sail
sail_mask_3.unsat.sail
sail_mask_4.unsat.sail
sail_mask_5.unsat.sail
scattered_enum.sail
scattered_enum_mod.sail
scattered_function_mod.sail
scattered_map_mod.sail
scattered_mapping.sail
scattered_mapping_doc.sail
scattered_union_doc.sail
scattered_union_mod.sail
scattered_union_rec.sail
set_match.sail
set_struct.sail
set_struct2.sail
set_syntax.sail
shadow_cleanup.sail
shadow_leak_check.sail
shadow_leak_infer.sail
shadow_let.sail
shift_or_concat.unsat.sail
shift_or_concat128.unsat.sail
shift_or_concat4.unsat.sail
shift_or_concat4_2.unsat.sail
shift_or_concat_1.sat.sail
shift_or_concat_2.sat.sail
shiftr_zero_1.sat.sail
shiftr_zero_1.unsat.sail
short_circuit.sail
short_circuit_bool_ex.sail
sign_extend.unsat.sail
sign_extend_2.unsat.sail
simple_if.sail
simple_record_access.sail
simple_scattered.sail
single_arg.sail
single_assign_in_block.sail
single_enum.sail
single_guard.sail
single_union.sail
sizeof_fixed.sail
small_slice.sail
some_none.sail
some_none_int.sail
spc_mappings.sail
special_annot.sail
split.sail
sqrt.sat.sail
sqrt.unsat.sail
stack_struct.sail
store_load.sat.sail
store_load_scattered.sat.sail
strict_var.sail
string.sat.sail
string.unsat.sail
string_append_non_exec.sail
string_literal_type.sail
string_of_bits.sail
string_of_bits2.sail
string_take.sail
struct.sail
struct_fn_arg.sail
struct_incomplete_literal.sail
struct_mapping.sail
struct_pattern.sail
struct_pattern_duplicate_field.sail
struct_pattern_partial.sail
struct_rec.sail
struct_update.sail
synonym_rec.sail
tautology.sail
test_if_comment_1.sail
tl_let.sail
tl_let_shadow.sat.sail
tl_pat.sail
tl_poly_match.sail
toplevel_let.unsat.sail
toplevel_let_trivial.unsat.sail
toplevel_tyvar.sail
trivial.sat.sail
trivial.unsat.sail
trivial_assert.sat.sail
trivial_assert_2.unsat.sail
trivial_funcall.sat.sail
trivial_return.sat.sail
trivial_return.unsat.sail
true_false.sail
try_return.sail
try_while_try.sail
tuple_assign.sail
tuple_bitvector_int_pat.sail
tuple_bitvector_int_pat2.sail
tuple_bitvector_int_pat3.sail
tuple_conversion.sail
tuple_fun.sail
tuple_type_cast.sail
tuple_union.sail
two_argument.sail
two_mapping.sail
type_div.sail
type_pow_zero.sail
tyvar_shadow.sail
unbalanced_comment.sail
unbalanced_comment2.sail
unbound_tyvar.sail
unbound_tyvar2.sail
unbounded_int_annot.sail
unconstructed_type_mono.sail
undeclared_field_assignment.sail
undeclared_vector_assignment.sail
undefined_infer.sail
undefined_nat.sail
undefined_union.sail
union_infer.sail
union_rec.sail
union_recf.sail
unknown_operator.sail
unscope_enum.sail
unscope_let.sail
unscope_register.sail
unscope_type.sail
unscope_val.sail
unsigned_index.sail
unterminated_ifdef.sail
unterminated_string.sail
unused_poly_ctor.sail
update_access.unsat.sail
update_subrange.unsat.sail
val.sail
varity.sail
varswap.sail
vec_length.sail
vec_length_inc.sail
vec_pat1.sail
vector_access.sail
vector_access_dec.sail
vector_append.sail
vector_append_gen.sail
vector_concat_assign.sail
vector_example.sail
vector_pattern_split.sail
vector_subrange_gen.sail
vector_subrange_pattern.sail
vmatch.sail
warl.sail
warl2.sail
warn_cannot_wildcard.sail
warn_cons_incomplete.sail
warn_cons_wildcard_insert1.sail
warn_cons_wildcard_insert2.sail
warn_double_cons_incomplete.sail
warn_empty_list.sail
warn_int_pattern.sail
warn_missing_enum.sail
warn_partial_lookup.sail
warn_partial_scattered.sail
warn_range_redundant.sail
warn_struct_pattern_incomplete.sail
warn_tuple_bitvector_pat.sail
warn_unbounded_int.sail
warn_unbounded_nat.sail
wf_assign_type.sail
wf_register_type.sail
wf_specs.sail
while_MM.sail
while_MP.sail
while_PM.sail
while_PP.sail
wildcard_mapping.sail
write_ref.sat.sail
write_ref.unsat.sail
xlen32.sail
xlen_val.sail
zero_length_bv.sail
zeros_1.sat.sail
zeros_1.unsat.sail
zeros_2.sat.sail
zeros_2.unsat.sail
zeros_3.sat.sail
zeros_3.unsat.sail
zeros_4.unsat.sail
zeros_mapping.sail
zeros_ones.unsat.sail