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