Verilog: fix strong release in word-level BMC

[kroening]

Fixes the false proof exposed by PR #1999 in the word-level BMC property encoding.

Summary:

• Correct strong_R(p, q) to F(p) and (p R q)
• Treat s_until_with as a lasso-requiring property for the infinite-path encoding
• Promote regression/verilog/SVA/strong_R1.desc from KNOWNBUG to CORE

Testing:

• ./src/ebmc/ebmc regression/verilog/SVA/strong_R1.sv --bound 20