Skip to content

GitLab

Open
Created by cameron@cameronMaintainer

Z3 failure with tokenizer

In branch newtokenizer at commit bd1f62d5, the following command generates a strange Z3 error message on both ARM (Apple Silicon) and X86/AVX-2. Z3 versions are v4.13.0 on ARM and v4.8.12 on X86.

bin/tokenizer --strings --vocab=../tools/lex/tokenizer_files/merges.txt --compact-base=5 --level-partition ~/Wikibooks/wiki-books-all.xml > fi2

The error occurs with any data file.

LLVM ERROR: Unexpected Z3 error when attempting to convert model value to number!
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information