Skip to content

Assertion violation at src/smt/smt_internalizer.cpp:1045 #3959

@wintered

Description

@wintered
[670] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_internalizer.cpp
Line: 1045
b_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[671] % 
[671] % z3release small.smt2
unsat
[672] % z3san small.smt2
=================================================================
==21960==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x60300001fd32 at pc 0x564e6388e966 bp 0x7fff18702260 sp 0x7fff18702250
READ of size 1 at 0x60300001fd32 thread T0
  #0 0x564e6388e965 in smt::context::get_lit_assignment(unsigned int) const ../src/smt/smt_context.h:362
  #1 0x564e6388e965 in smt::context::get_assignment(smt::literal) const ../src/smt/smt_context.h:366
  #2 0x564e6388e965 in smt::context::assign(smt::literal, smt::b_justification const&, bool) ../src/smt/smt_context.h:946
  #3 0x564e638b0ffc in smt::context::init_assumptions(ref_vector<expr, ast_manager> const&) ../src/smt/smt_context.cpp:3217
  #4 0x564e638bcc81 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3482
  #5 0x564e6500d2b7 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #6 0x564e64fca8d3 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:213
  #7 0x564e64fabdb1 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #8 0x564e64f06e10 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1551
  #9 0x564e64e4a5f3 in smt2::parser::parse_check_sat_assuming() ../src/parsers/smt2/smt2parser.cpp:2609
  #10 0x564e64e4df27 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2982
  #11 0x564e64e4df27 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #12 0x564e64e04fa5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #13 0x564e624c5426 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #14 0x564e6249df2e in main ../src/shell/main.cpp:352
  #15 0x7f4bfd711b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #16 0x564e624b1a99 in _start (z3san/build-04132020190805-0f69783/z3+0x1f6a99)
...
==21960==ABORTING
[673] % 
[673] % cat small.smt2
(check-sat-assuming (or true))
[674] %

OS: Ubuntu 18.04
Commit: 0f69783

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions