With_Expr in array_literal refers to unimplemented type (integer)

[xbauch]

For the follow Ada code:

procedure Arrays is
   subtype Range1 is Integer range 10 .. 20;
   type Arr3 is array (Range1) of Integer;
   Actual3 : Arr3 := (7, 8, 9, others => 10);
begin
   pragma Assert(Actual3(14)=15);
end Arrays;

CBMC crashes with:

Starting program: /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc arrays.json_symtab
CBMC version 5.11 (cbmc-5.11-850-g71bdebf63) 64-bit x86_64 linux
Parsing arrays.json_symtab
Converting
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
size of program expression: 67 steps
simple slicing removed 2 assignments
Generated 4 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
--- begin invariant violation report ---
Invariant check failed
File: /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/solvers/flattening/boolbv_width.cpp:198 function: get_entry
Condition: false
Reason: Unimplemented
Backtrace:
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(print_backtrace(std::ostream&)+0x4d) [0x55555614c3ba]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(get_backtrace[abi:cxx11]()+0x45) [0x55555614c5c1]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x4c) [0x555555b74689]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(+0x61f165) [0x555555b73165]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbv_widtht::get_entry(typet const&) const+0x12ee) [0x555555fb9192]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbv_widtht::operator()(typet const&) const+0x23) [0x555555f84c8f]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbvt::convert_constant(constant_exprt const&)+0x60) [0x555555f92608]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbvt::convert_bitvector(exprt const&)+0x575) [0x555555f7bb63]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bv_pointerst::convert_bitvector(exprt const&)+0xf14) [0x555555fc5406]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0x100) [0x555555f7afb4]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbvt::convert_index(index_exprt const&)+0x297) [0x555555fa1a4d]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbvt::convert_bitvector(exprt const&)+0x123) [0x555555f7b711]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bv_pointerst::convert_bitvector(exprt const&)+0xf14) [0x555555fc5406]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbvt::convert_bv(exprt const&, nonstd::optional_lite::optional<unsigned long>)+0x100) [0x555555f7afb4]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbvt::convert_equality(equal_exprt const&)+0x2e8) [0x555555f95b26]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbvt::convert_rest(exprt const&)+0x1fe) [0x555555f7deaa]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bv_pointerst::convert_rest(exprt const&)+0x898) [0x555555fc0356]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(prop_conv_solvert::convert_bool(exprt const&)+0x13ec) [0x555555ff4ab6]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(prop_conv_solvert::convert(exprt const&)+0x19d) [0x555555ff3619]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(arrayst::add_array_constraint(arrayst::lazy_constraintt const&, bool)+0x12c) [0x555555f70bd0]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(arrayst::add_array_constraints_with(std::set<exprt, std::less<exprt>, std::allocator<exprt> > const&, with_exprt const&)+0x261) [0x555555f728a3]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(arrayst::add_array_constraints(std::set<exprt, std::less<exprt>, std::allocator<exprt> > const&, exprt const&)+0x7d) [0x555555f71b05]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(arrayst::add_array_constraints()+0xdc) [0x555555f70cd6]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(arrayst::post_process_arrays()+0x18) [0x555555bca65e]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(arrayst::post_process()+0x25) [0x555555bca637]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(boolbvt::post_process()+0x36) [0x555555f85054]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bv_pointerst::post_process()+0x27) [0x555555fc78c5]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(prop_conv_solvert::dec_solve()+0x75) [0x555555ff5a19]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(cover_goalst::operator()()+0x83) [0x555555feea3f]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmc_all_propertiest::operator()()+0x6be) [0x555555bb28e4]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmct::all_properties(goto_functionst const&)+0x8b) [0x555555bb42ff]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmct::decide(goto_functionst const&)+0xe7) [0x555555b89f67]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmct::execute(abstract_goto_modelt&)+0x8a6) [0x555555b89942]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmct::run(abstract_goto_modelt&)+0xb4) [0x555555b89e6a]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(bmct::do_language_agnostic_bmc(optionst const&, abstract_goto_modelt&, ui_message_handlert&, std::function<void (bmct&, symbol_tablet const&)>, std::function<bool ()>)+0x2d3) [0x555555b8a8b3]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(cbmc_parse_optionst::doit()+0xa1b) [0x555555b7c53f]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(parse_options_baset::main()+0x10f) [0x5555561718a7]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(main+0x55) [0x555555b72ebf]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xe7) [0x7ffff70c6b97]
/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/build/bin/cbmc(_start+0x2a) [0x555555b72d8a]


--- end invariant violation report ---

Program received signal SIGABRT, Aborted.
__GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:51
51	../sysdeps/unix/sysv/linux/raise.c: No such file or directory.
(gdb) up
#1  0x00007ffff70e5801 in __GI_abort () at abort.c:79
79	abort.c: No such file or directory.
(gdb) 
#2  0x0000555555b746f0 in invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&> (
    file="/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/solvers/flattening/boolbv_width.cpp", function="get_entry", line=198, condition="false", params#0="Unimplemented")
    at /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/util/invariant.h:236
236	  abort();
(gdb) 
#3  0x0000555555b73165 in invariant_violated_string (file="/home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/solvers/flattening/boolbv_width.cpp", function="get_entry", line=198, condition="false", 
    reason="Unimplemented") at /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/util/invariant.h:257
257	  invariant_violated_structured<invariant_failedt>(
(gdb) 
#4  0x0000555555fb9192 in boolbv_widtht::get_entry (this=0x555556906698, type=...) at /home/diffblue/petr.bauch/code/gnat2goto/lib/cbmc/src/solvers/flattening/boolbv_width.cpp:198
198	    UNIMPLEMENTED;
(gdb) call puts(type.pretty(0,0).c_str())
integer