z3 refutation crash - fatal error: error in backend: Z3 error: operator is applied to arguments of the wrong sort

The simple reproducer

```
void z3_crash(long a) {
if (~-(5 && a)) {
long *c;
*c; // expected-warning{{Dereference of undefined pointer value (loaded from variable 'c')}}
}
}
```

To run:

```clang --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true z3.c ```

The crashstack
```
fatal error: error in backend: Z3 error: operator is applied to arguments of the wrong sort
PLEASE submit a bug report to https://github.com/llvm/llvm-project/issues/ and include the crash backtrace, preprocessed source, and associated run script.
Stack dump:
0. Program arguments: clang --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true z3.c
1. parser at end of file
#0 0x0000000004163fa8 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (clang+0x4163fa8)
#1 0x00000000041613cc llvm::sys::CleanupOnSignal(unsigned long) (clang+0x41613cc)
#2 0x00000000040a5cc6 llvm::CrashRecoveryContext::HandleExit(int) (clang+0x40a5cc6)
#3 0x000000000415889e llvm::sys::Process::Exit(int, bool) (clang+0x415889e)
#4 0x0000000000dc1e10 LLVMErrorHandler(void*, char const*, bool) cc1_main.cpp:0:0
#5 0x00000000040b0fc3 llvm::report_fatal_error(llvm::Twine const&, bool) (clang+0x40b0fc3)
#6 0x000000000879cb93 (anonymous namespace)::Z3ErrorHandler(_Z3_context*, Z3_error_code) Z3Solver.cpp:0:0
#7 0x00007f89c4d8e0bd Z3_mk_bvnot (libz3.so+0x12a0bd)
#8 0x000000000879ac22 (anonymous namespace)::Z3Solver::mkBVNot(llvm::SMTExpr const* const&) Z3Solver.cpp:0:0
#9 0x0000000006481892 clang::ento::SMTConv::getSymExpr(std::shared_ptr&, clang::ASTContext&, clang::ento::SymExpr const*, clang::QualType*, bool*) (clang+0x6481892)
#10 0x00000000064a5efd clang::ento::SMTConv::getRangeExpr(std::shared_ptr&, clang::ASTContext&, clang::ento::SymExpr const*, llvm::APSInt const&, llvm::APSInt const&, bool) (.constprop.0) Z3CrosscheckVisitor.cpp:0:0
#11 0x00000000064ab72f clang::ento::Z3CrosscheckVisitor::finalizeVisitor(clang::ento::BugReporterContext&, clang::ento::ExplodedNode const*, clang::ento::PathSensitiveBugReport&) (clang+0x64ab72f)
#12 0x000000000631cd54 generateVisitorsDiagnostics(clang::ento::PathSensitiveBugReport*, clang::ento::ExplodedNode const*, clang::ento::BugReporterContext&) BugReporter.cpp:0:0
#13 0x000000000631f7c8 (anonymous namespace)::PathDiagnosticBuilder::findValidReport(llvm::ArrayRef&, clang::ento::PathSensitiveBugReporter&) BugReporter.cpp:0:0
#14 0x0000000006327720 clang::ento::PathSensitiveBugReporter::generatePathDiagnostics(llvm::ArrayRef>>, llvm::ArrayRef&) (clang+0x6327720)
#15 0x0000000006328221 clang::ento::PathSensitiveBugReporter::generateDiagnosticForConsumerMap(clang::ento::BugReport*, llvm::ArrayRef>>, llvm::ArrayRef) (clang+0x6328221)
#16 0x00000000063246f7 clang::ento::BugReporter::FlushReport(clang::ento::BugReportEquivClass&) (clang+0x63246f7)
#17 0x000000000632570f clang::ento::BugReporter::FlushReports() (clang+0x632570f)
#18 0x0000000005f1e3c0 (anonymous namespace)::AnalysisConsumer::HandleCode(clang::Decl*, unsigned int, clang::ento::ExprEngine::InliningModes, llvm::DenseSet>*) AnalysisConsumer.cpp:0:0
#19 0x0000000005f1fc2f (anonymous namespace)::AnalysisConsumer::HandleTranslationUnit(clang::ASTContext&) AnalysisConsumer.cpp:0:0
#20 0x00000000064ee7dc clang::ParseAST(clang::Sema&, bool, bool) (clang+0x64ee7dc)
#21 0x0000000004daeaf5 clang::FrontendAction::Execute() (clang+0x4daeaf5)
#22 0x0000000004d2fc7e clang::CompilerInstance::ExecuteAction(clang::FrontendAction&) (clang+0x4d2fc7e)
#23 0x0000000004ea788d clang::ExecuteCompilerInvocation(clang::CompilerInstance*) (clang+0x4ea788d)
#24 0x0000000000dc4540 cc1_main(llvm::ArrayRef, char const*, void*) (clang+0xdc4540)
#25 0x0000000000dbb0ea ExecuteCC1Tool(llvm::SmallVectorImpl&, llvm::ToolContext const&, llvm::IntrusiveRefCntPtr) driver.cpp:0:0
#26 0x0000000000dbb26d int llvm::function_ref&)>::callback_fn&)>(long, llvm::SmallVectorImpl&) driver.cpp:0:0
#27 0x0000000004b2b169 void llvm::function_ref::callback_fn>, std::__cxx11::basic_string, std::allocator>*, bool*) const::'lambda'()>(long) Job.cpp:0:0
#28 0x00000000040a5c04 llvm::CrashRecoveryContext::RunSafely(llvm::function_ref) (clang+0x40a5c04)
#29 0x0000000004b2b77f clang::driver::CC1Command::Execute(llvm::ArrayRef>, std::__cxx11::basic_string, std::allocator>*, bool*) const (.part.0) Job.cpp:0:0
#30 0x0000000004aec5c2 clang::driver::Compilation::ExecuteCommand(clang::driver::Command const&, clang::driver::Command const*&, bool) const (clang+0x4aec5c2)
#31 0x0000000004aed56e clang::driver::Compilation::ExecuteJobs(clang::driver::JobList const&, llvm::SmallVectorImpl>&, bool) const (clang+0x4aed56e)
#32 0x0000000004af4cc5 clang::driver::Driver::ExecuteCompilation(clang::driver::Compilation&, llvm::SmallVectorImpl>&) (clang+0x4af4cc5)
#33 0x0000000000dc0a31 clang_main(int, char**, llvm::ToolContext const&) (clang+0xdc0a31)
#34 0x0000000000c7eea4 main (clang+0xc7eea4)
#35 0x00007f89c3a937e5 __libc_start_main (/lib64/libc.so.6+0x3a7e5)
#36 0x0000000000dbab8e _start (clang+0xdbab8e)
clang: error: clang frontend command failed with exit code 70 (use -v to see invocation)
clang version 22.0.0git (https://github.com/llvm/llvm-project.git 87616939190b1c0d322f0f3c1d69ba3626d18582)
Target: x86_64-unknown-linux-gnu
Thread model: posix

```