Stuck rewriting in rewrite_eq_exp

[jix]

When using boolector as backend for yosys-smtbmc, I encountered an input for which boolector hangs essentially forever during the initial rewrite for a (define-fun ...), even before the following (check-sat) is issued. I manually minimized the yosys-smtbmc generated SMT2 by removing everything unnecessary to trigger this behavior. I then reduced the width of the involved signals from 32 to 24 bits. With 24 bits, it does get past the (define-fun ...) but still takes 30 seconds just to process it. Both variants are attached. When I take a stack trace during the rewriting, I see deeply nested rewrite_eq_exp calls. I tested with the latest master version of boolector.

This seems similar to #11, but since a fix for that was committed and I still see similar behavior with the latest version of boolector, I decided to file a new issue.

hang_min_32.smt2.txt
hang_min_24.smt2.txt

[mpreiner]

Boolector is not actively maintained and developed anymore. It was succeeded by Bitwuzla and the repository is now archived.