Zhendong Su

It appears to be a recent regression. Compiler Explorer: https://godbolt.org/z/TEqGhcT7r ``` [507] % clangtk -v clang version 16.0.0 (https://github.com/llvm/llvm-project.git de6fd169715764f0401d8580b64c11fda45101e1) Target: x86_64-unknown-linux-gnu Thread model: posix InstalledDir: /local/suz-local/opfuzz/bin Found candidate GCC...

clang crashes on valid code at -O3 on x86_64-linux-gnu: Assertion `N->getOpcode() != ISD::DELETED_NODE && RV.getOpcode() != ISD::DELETED_NODE && "Node was deleted but visit returned new node!"' failed

10

| | | | --- | --- | | Bugzilla Link | [51298](https://llvm.org/bz51298) | | Version | trunk | | OS | All | | CC | @RKSimon,@rotateright | ##...

clang crashes on valid C++ code: Assertion `!Friend->isDependentContext() && "can't handle friends with dependent contexts here"' failed

5

| | | | --- | --- | | Bugzilla Link | [27312](https://llvm.org/bz27312) | | Version | trunk | | OS | All | | CC | @DougGregor | ##...

``` [578] % z3release model_validate=true small.smt2 sat sat sat sat sat (error "line 16 column 10: an invalid model was generated") ( (define-fun a () Bool false) (define-fun s ()...

Commit: https://github.com/Z3Prover/z3/commit/278d5a348217951b5f52729fd0ca6110eddd2426 OS: Ubuntu 22.04 ``` [513] % z3release model_validate=true small.smt2 sat (error "line 5 column 10: an invalid model was generated") ( (define-fun b () String "1003") (define-fun a...

ASSERTION VIOLATION, File: ../src/math/polynomial/algebraic_numbers.cpp, Line: 2462

2

Commit: https://github.com/Z3Prover/z3/commit/e8929041b840ce7d04df8ce101d408042d2a4384 OS: Ubuntu 22.04 ``` [548] % z3debug small.smt2 ASSERTION VIOLATION File: ../src/math/polynomial/algebraic_numbers.cpp Line: 2462 !nested_call (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [549] % cat small.smt2 (declare-fun...

invalid model issue on an incremental string formula

11

``` [659] % z3release model_validate=true small.smt2 sat sat sat sat sat sat sat sat sat sat sat sat sat (error "line 27 column 10: an invalid model was generated") (...

[consolidated] hang on small instances (string, bit-vector)

10

Commit: https://github.com/Z3Prover/z3/commit/0b3bbc297248849cb17c29e0fbaa23f61bb45716 OS: Ubuntu 22.04 ``` [523] % time z3-4.11.2 small.smt2 sat real 0m0.112s user 0m0.035s sys 0m0.009s [524] % timeout -s 9 10 z3release small.smt2 Killed [525] % cat...