Nikolaj Bjorner

``` $ cat small.smt2 (declare-fun b (Real Real) Real) (declare-fun u (Real Real) (Array Real Real)) (assert (forall ((v Real) (r Real)) (= v (select (u v (b 0.0 0.0))...

``` [554] % z3debug small.smt2 sat [555] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2 ASSERTION VIOLATION File: ../src/qe/qsat.cpp Line: 636 validate_defs("check_sat") (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [556] % cat...

This must be a regression, maybe due to newer versions of MacOS on the build machines. The build machines use a "fake" macos version. It is the one you see....

6cd619d377d829a81249cef93279afebcd945b44

Could you dry-run the nigthly? https://github.com/Z3Prover/z3/releases/tag/Nightly

the new release uses the 11_0 naming scheme

it doesn't repro for me (but not on your arch/opsys). What is your architecture? Specifically pointer alignment may be at stake.

The reproducer does not crash on my side. It did exhibit an issue with the parser. It should have failed earlier when reading the ")". This was fixed. I have...

The asan heap sanitizer does not suggest any memory corruptions. Your environment may be dealing with a pointer alignment assumption, such as 128 bit alignment?

Thanks, I know what the bug is (a regression), but don't have a fix right now