You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
z3 test.smt2
info:
sat
sat
AddressSanitizer:DEADLYSIGNAL
=================================================================
==3389739==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x5555576592fb bp 0x7fffffffdd78 sp 0x7fffffffd140 T0)
==3389739==The signal is caused by a READ memory access.
==3389739==Hint: address points to the zero page.
#0 0x5555576592fb in sat::literal::var() const /yuhao/z3/build/../src/util/sat_literal.h:51:20
#1 0x5555576592fb in sat::solver::user_pop(unsigned int) /yuhao/z3/build/../src/sat/sat_solver.cpp:3716:58
#2 0x555555e7ce84 in inc_sat_solver::pop(unsigned int) /yuhao/z3/build/../src/sat/sat_solver/inc_sat_solver.cpp:278:18
#3 0x555556ce0e99 in cmd_context::pop(unsigned int) /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:1702:19
#4 0x555556c867ba in smt2::parser::parse_pop() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:2572:19
#5 0x555556c7ff57 in smt2::parser::operator()() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:3191:29
#6 0x555556c7f16c in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:3242:12
#7 0x55555572469e in read_smtlib2_commands(char const*) /yuhao/z3/build/../src/shell/smtlib_frontend.cpp:182:18
#8 0x555555749c96 in main /yuhao/z3/build/../src/shell/main.cpp:384:28
#9 0x7ffff7a6dd8f (/lib/x86_64-linux-gnu/libc.so.6+0x29d8f) (BuildId: 962015aa9d133c6cbcfb31ec300596d7f44d3348)
#10 0x7ffff7a6de3f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x29e3f) (BuildId: 962015aa9d133c6cbcfb31ec300596d7f44d3348)
#11 0x555555642e44 in _start (/yuhao/z3/build/z3+0xeee44) (BuildId: c849818b1aebb32cb9f0222cdd142430bf37dac7)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV /yuhao/z3/build/../src/util/sat_literal.h:51:20 in sat::literal::var() const
==3389739==ABORTING
cat test.smt2
(check-sat)
(push)
(set-logic QF_BV)
(set-option :produce-models true)
(declare-const a (_ BitVec 8))
(check-sat)
(pop)
(declare-const b (_ BitVec 8))
(check-sat)
The same for other similar push operations.If the push operation cannot be performed before set-logic, it should not return a segfault.There should be processing logic to prohibit it
The text was updated successfully, but these errors were encountered:
Hi!
Z3 [version 4.13.1 - 64 bit].
ubuntu:22.04
The same for other similar push operations.If the push operation cannot be performed before set-logic, it should not return a segfault.There should be processing logic to prohibit it
The text was updated successfully, but these errors were encountered: