Yosys sat -prove segfaults on a design containing a memory read

### Version 0.66 ### On which OS did this happen? macOS ### Reproduction Steps Version: Yosys 0.66 (git sha1 7f8fdfd8d7bc08c749a2a969388d3425d4f369d5), clang++ 21.0.0, macOS (Apple silicon, Homebrew build). Command (SIGSEGV, exit 139): yosys -p "read_rtlil bug.il; memory; sat -prove out 8'00000101" Minimal bug.il — a module whose only output is an asynchronous read of an uninitialized memory: module \top wire width 4 input 1 \addr wire width 8 output 2 \out wire width 8 $r memory width 8 size 16 \mem cell $memrd $rd parameter \MEMID "\\mem" parameter \ABITS 4 parameter \WIDTH 8 parameter \CLK_ENABLE 0 parameter \CLK_POLARITY 0 parameter \TRANSPARENT 0 connect \CLK 1'x connect \EN 1'x connect \ADDR \addr connect \DATA $r end connect \out $r end Isolation notes (all on the same bug.il): - read_rtlil bug.il; memory → OK (exit 0). The crash is not in read_rtlil or memory. - read_rtlil bug.il; memory; sat (find-a-model) → OK (exit 0). - read_rtlil bug.il; memory; sat -prove out 8'00000101 → SIGSEGV. - read_rtlil bug.il; memory_collect; memory_map; sat -prove … → also SIGSEGV. - Adding/removing a $meminit, and the specific prove-value, make no difference — the crash is the sat -prove path over a $memrd-derived signal (present regardless of whether memory mapped it to logic). So: sat succeeds but sat -prove crashes on the identical circuit, whenever the proven signal derives from a memory read. bug.il is at .../scratchpad/bug.il if you want the exact file to attach. ### Expected Behavior No SIGSEGV ### Actual Behavior SIGSEGV