SMT2: avoid emitting unary bitvector concat

[kroening]

When zero-width operands are dropped from a concatenation expression, the remaining operands may reduce to a single one. Previously this produced invalid (concat x) in the SMT-LIB output. Now the single operand is emitted directly.

Changes

• src/solvers/smt2/smt2_conv.cpp: Collect non-zero-width operands first; emit directly if only one remains.
• unit/solvers/smt2/smt2_conv.cpp: Add unit test with a zero-width bitvector operand asserting the generated string.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.51%. Comparing base (4993eb9) to head (425b797).
⚠️ Report is 2 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8997      +/-   ##
===========================================
- Coverage    80.51%   80.51%   -0.01%     
===========================================
  Files         1704     1704              
  Lines       188874   188885      +11     
  Branches        73       73              
===========================================
+ Hits        152076   152083       +7     
- Misses       36798    36802       +4     

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

[tautschnig]

After the DATA_INVARIANT on line 1310 guarantees !non_zero_width_ops.empty(), the only value that satisfies size() <= 1 is size() == 1:

Suggested change

	if(non_zero_width_ops.size() <= 1)
	{
	// unary concat is not valid SMT-LIB; emit the operand directly
	if(non_zero_width_ops.size() == 1)
	flatten2bv(non_zero_width_ops.front());
	}
	if(non_zero_width_ops.size() == 1)
	{
	// unary concat is not valid SMT-LIB; emit the operand directly
	flatten2bv(non_zero_width_ops.front());
	}

[kroening]

Done