Support 1-bit signed bitvectors in bv_utilst::lt_or_le

[kroening]

The compact signed comparison encoding in lt_or_le required at least 2 bits, rejecting 1-bit signed bitvectors with an INVARIANT failure. A 1-bit signed bitvector represents {0, -1}, so comparison reduces to sign-bit logic.

Changes

• Add early return for the 1-bit signed case before the compact encoding
• Reword the INVARIANT message to clarify it applies to the compact encoding
• Add unit test covering constant and symbolic 1-bit signed comparisons (< and <=)

Testing

• New unit test: unit/solvers/flattening/bv_utils.cpp (6 assertions, all pass)
• Existing unit tests pass

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.52%. Comparing base (4993eb9) to head (648e9ae).
⚠️ Report is 4 commits behind head on develop.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8998   +/-   ##
========================================
  Coverage    80.51%   80.52%           
========================================
  Files         1704     1705    +1     
  Lines       188874   188927   +53     
  Branches        73       73           
========================================
+ Hits        152076   152131   +55     
+ Misses       36798    36796    -2     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.