Segfault is triggered when push is before logic set

Hi! Z3 [version 4.13.1 - 64 bit]. ubuntu:22.04

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

Z3Prover / z3

Segfault is triggered when push is before logic set #7246