Exception while running typefuzz on the remote server

[BritikovKI]

Bug Description

While trying to use typefuzz on Ubuntu Linux

Linux mantella 5.4.0-159-generic #176-Ubuntu SMP Mon Aug 14 12:04:20 UTC 2023 x86_64 x86_64 x86_64 GNU/Linux

It returns an error, trying to iterate on argument of type "Term"

Note

Possibly it is due to the command, as cvc5 is not installed on the machine, and I try to provide it by giving the executable path in the command:

./bin/typefuzz "z3 model_validate=true;../cvc5/build/bin/cvc5 --check-models -m -i -q" ../opensmt/regression/QF_UF/NEQ004_size4.smt│2

[wintered]

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

[BritikovKI]

Hi @wintered, thanks for the quick response. I tried to run it with QF_LIA, but stubled into a different error

Any ideas what could have caused it?

[wintered]

@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.