Segmentation fault

[daniel-larraz]

The attached input causes z3 (4.8.3) to produce a segmentation fault.

Additional remarks:

• The issue also occurs with z3 4.8.1, but not with z3 4.7.1
• Removing the set-logic command from the file prevents the issue from happening

[NikolajBjorner]

@levnach can you take a look?

[levnach]

A term is being added to lar_solver with column j = 2 which is not known to lar_solver at this moment.
I am seeing the stack below.
#1 0x000000000070d9f8 in vector<lp::ext_var_info, false, unsigned int>::operator[] (this=0x2149cc8, idx=2) at ../../src/util/vector.h:373
#2 0x00000000007297c8 in lp::var_register::local_is_int (this=0x2149cc8, j=2) at ../../src/util/lp/var_register.h:98
#3 0x00000000007216c7 in lp::lar_solver::column_is_int (this=0x2149ad8, j=2) at ../../src/util/lp/lar_solver.cpp:1504
#4 0x00000000007215e0 in lp::lar_solver::term_is_int (this=0x2149ad8, t=0x2154660) at ../../src/util/lp/lar_solver.cpp:1488
#5 0x000000000072237a in lp::lar_solver::add_row_from_term_no_constraint (this=0x2149ad8, term=0x2154660, term_ext_index=1000000) at ../../src/util/lp/lar_solver.cpp:1650
#6 0x0000000000722162 in lp::lar_solver::add_term (this=0x2149ad8, coeffs=...) at ../../src/util/lp/lar_solver.cpp:1640
#7 0x0000000001280e1c in smt::theory_lra::imp::internalize_linearized_def (this=0x2149458, term=0x20d3fa8, st=...) at ../../src/smt/theory_lra.cpp:829
#8 0x0000000001280987 in smt::theory_lra::imp::internalize_def (this=0x2149458, term=0x20d3fa8) at ../../src/smt/theory_lra.cpp:805
#9 0x0000000001282750 in smt::theory_lra::imp::internalize_term (this=0x2149458, term=0x20d3fa8) at ../../src/smt/theory_lra.cpp:929
#10 0x000000000127b461 in smt::theory_lra::internalize_term (this=0x2148d08, term=0x20d3fa8) at ../../src/smt/theory_lra.cpp:3439
#11 0x0000000000fe3deb in smt::context::internalize_theory_term (this=0x2109648, n=0x20d3fa8) at ../../src/smt/smt_internalizer.cpp:821
#12 0x0000000000fe32c5 in smt::context::internalize_term (this=0x2109648, n=0x20d3fa8) at ../../src/smt/smt_internalizer.cpp:760
#13 0x0000000000fe0787 in smt::context::internalize (this=0x2109648, n=0x20d3fa8, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:341
#14 0x0000000000fe3519 in smt::context::internalize_ite_term (this=0x2109648, n=0x20d4008) at ../../src/smt/smt_internalizer.cpp:786
#15 0x0000000000fe32ad in smt::context::internalize_term (this=0x2109648, n=0x20d4008) at ../../src/smt/smt_internalizer.cpp:757
#16 0x0000000000fe0787 in smt::context::internalize (this=0x2109648, n=0x20d4008, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:341
#17 0x0000000000fe3537 in smt::context::internalize_ite_term (this=0x2109648, n=0x20d4068) at ../../src/smt/smt_internalizer.cpp:787
#18 0x0000000000fe32ad in smt::context::internalize_term (this=0x2109648, n=0x20d4068) at ../../src/smt/smt_internalizer.cpp:757
#19 0x0000000000fe0787 in smt::context::internalize (this=0x2109648, n=0x20d4068, gate_ctx=false) at ../../src/smt/smt_internalizer.cpp:341
#20 0x000000000127f763 in smt::theory_lra::imp::mk_var (this=0x2149458, n=0x20d4068, internalize=true) at ../../src/smt/theory_lra.cpp:635
#21 0x000000000127e8fa in smt::theory_lra::imp::linearize (this=0x2149458, st=...) at ../../src/smt/theory_lra.cpp:519
#22 0x000000000127da7f in smt::theory_lra::imp::linearize_term (this=0x2149458, term=0x2110a38, st=...) at ../../src/smt/theory_lra.cpp:394
#23 0x0000000001280970 in smt::theory_lra::imp::internalize_def (this=0x2149458, term=0x2110a38) at ../../src/smt/theory_lra.cpp:804
#24 0x0000000001282162 in smt::theory_lra::imp::internalize_atom (this=0x2149458, atom=0x20d36a8, gate_ctx=true) at ../../src/smt/theory_lra.cpp:897
#25 0x000000000127b438 in smt::theory_lra::internalize_atom (this=0x2148d08, atom=0x20d36a8, gate_ctx=true) at ../../src/smt/theory_lra.cpp:3436
#26 0x0000000000fe19ae in smt::context::internalize_theory_atom (this=0x2109648, n=0x20d36a8, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:452
#27 0x0000000000fe1010 in smt::context::internalize_formula (this=0x2109648, n=0x20d36a8, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:395
#28 0x0000000000fe06a9 in smt::context::internalize (this=0x2109648, n=0x20d36a8, gate_ctx=true) at ../../src/smt/smt_internalizer.cpp:333
#29 0x0000000000fdfa6c in smt::context::assert_default (this=0x2109648, n=0x20d36a8, pr=0x0) at ../../src/smt/smt_internalizer.cpp:278
#30 0x0000000000fdf99e in smt::context::internalize_assertion (this=0x2109648, n=0x20d36a8, pr=0x0, generation=0) at ../../src/smt/smt_internalizer.cpp:273
#31 0x0000000000fa70ba in smt::context::internalize_assertions (this=0x2109648) at ../../src/smt/smt_context.cpp:3126
#32 0x0000000000fa97e2 in smt::context::check (this=0x2109648, num_assumptions=0, assumptions=0x0, reset_cancel=true) at ../../src/smt/smt_context.cpp:3437
#33 0x0000000000ff4dd5 in smt::kernel::imp::check (this=0x2109648, num_assumptions=0, assumptions=0x0) at ../../src/smt/smt_kernel.cpp:115
#34 0x0000000000ff2f6f in smt::kernel::check (this=0x21092e8, num_assumptions=0, assumptions=0x0) at ../../src/smt/smt_kernel.cpp:289
#35 0x000000000105e913 in smt::smt_solver::check_sat_core (this=0x2108f98, num_assumptions=0, assumptions=0x0) at ../../src/smt/smt_solver.cpp:190
#36 0x0000000000c9ac51 in solver_na2as::check_sat (this=0x2108f98, num_assumptions=0, assumptions=0x20d3110) at ../../src/solver/solver_na2as.cpp:67
#37 0x0000000000c8d61a in combined_solver::check_sat (this=0x2107e18, num_assumptions=0, assumptions=0x20d3110) at ../../src/solver/combined_solver.cpp:236
#38 0x0000000000d9bccb in cmd_context::check_sat (this=0x7fffffffdf30, num_assumptions=0, assumptions=0x20d3110) at ../../src/cmd_context/cmd_context.cpp:1574
#39 0x0000000000debed9 in smt2::parser::parse_check_sat (this=0x7fffffffd450) at ../../src/parsers/smt2/smt2parser.cpp:2630
#40 0x0000000000dee051 in smt2::parser::parse_cmd (this=0x7fffffffd450) at ../../src/parsers/smt2/smt2parser.cpp:2966
#41 0x0000000000def1b8 in smt2::parser::operator() (this=0x7fffffffd450) at ../../src/parsers/smt2/smt2parser.cpp:3141
#42 0x0000000000dd9370 in parse_smt2_commands (ctx=..., is=..., interactive=false, ps=..., filename=0x0) at ../../src/parsers/smt2/smt2parser.cpp:3190
#43 0x00000000018e1019 in read_smtlib2_commands (file_name=0x7fffffffe776 "/home/lev/Dropbox/bug.smt2") at ../../src/shell/smtlib_frontend.cpp:95
#44 0x00000000018df8f7 in main (argc=2, argv=0x7fffffffe3b8) at ../../src/shell/main.cpp:353