Dominik Winterer

We do not plan to support performance fuzzing any time soon.

``` (declare-fun a () Real) (declare-fun b () Real) (declare-fun c () Real) (declare-fun d () Real) (declare-fun e () Real) (assert (not (exists ((f Real)) (=> (and (= c...

Another repro. ``` [677] % cvc4 -q small.smt2 unsat [678] % z3 small.smt2 sat [679] % [679] % cat small.smt2 (declare-fun a () Real) (declare-fun b () Real) (declare-fun c...

``` $z3release model_validate=true bug.smt2 sat (error "line 5 column 10: an invalid model was generated") $cat bug.smt2 (declare-fun T_2 () Bool) (declare-fun var_0xINPUT_540541 () String) (assert (= T_2 (= 1...

Hi @BritikovKI, this error occurs because the type-checker is still incomplete, i.e. does not fully support QF_UF yet.

@BritikovKI this isn't an error in the tool; You seem to have found a bug in z3. Inspect the bugs folder and inspect the .output and .smt2.

@benjaminfjones no above link is not the commit I bisected to. It is the commit where the bug triggers.

Thanks @sarsko for the speedy reply; the corrected formula still leads to the panic. ``` $CreuSAT --file f.cnf c Reading file 'f.cnf' c Parsed formula with 1 clauses and 1...

@sarsko I'll close this now. Feel free to reopen, should it become relevant.

[ef82847](https://github.com/cvc5/cvc5/commit/ef828478cf4834ff95c787fb0d3354e326caa097) ```` $ cvc5 -q --check-proofs bug.smt2 cvc5 suffered a segfault. Offending address is 0x0 Looks like a NULL pointer was dereferenced. $ cat bug.smt2 (declare-fun x () String) (declare-fun...