[tautschnig]

cvc5 accepts `((as const (Array I E)) v)' only when v is a value ("invalid argument ... for 'val', expected a value"); z3 accepts any term. Two places wrote a term there:

• unflatten, turning a bit-vector (e.g. a union member such as the local buffer of std::string) back into an array, used the array's element 0 -- an extract of a term -- as the default. For a solver that requires a value (as_const_requires_value, set for cvc5) the base array is now all-zero (convert_zero_value builds the value in the sort unflatten produces) and every element 0..N-1 is stored.
• array_of with a non-literal element; it now takes the quantified initialisation used without `as const' (as_const_admits).

Test: regression/cbmc/smt2_cvc5_as_const_value (cbmc --cvc5 reported a parse error; it now verifies, and a wrong assertion fails).

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota. Try requesting a review at a lower effort level.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing. Review the Copilot code review billing settings.

[codecov]

Codecov Report

❌ Patch coverage is 56.36364% with 24 lines in your changes missing coverage. Please review.
✅ Project coverage is 81.03%. Comparing base (826c1c7) to head (c0f846d).
⚠️ Report is 6 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/solvers/smt2/smt2_conv.cpp	56.36%	24 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9419   +/-   ##
========================================
  Coverage    81.02%   81.03%           
========================================
  Files         1723     1723           
  Lines       191314   191379   +65     
  Branches        73       73           
========================================
+ Hits        155020   155080   +60     
- Misses       36294    36299    +5     

☔ View full report in Codecov by Harness.
📢 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]

This PR makes cvc5 lose counterexamples for arrays initialised with null pointers. The cause is that as_const_admits rejects pointer-typed constants.

Cause. convert_constant always prints a pointer-typed constant_exprt as a bit-vector literal: (_ bv0 w) for null, (_ bvN w) otherwise. cvc5 accepts that as a value under as const. However, as_const_admits does not list ID_pointer, so array_of(NULL) now takes the quantified substitute (assert (forall ((i ...)) (= (select array_of.N i) (_ bv0 64)))). The "object/offset encoding" mentioned in the comment applies to address_of terms, but those are not constant_exprt and are already rejected by is_constant().

Consequence. cvc5 1.3.4 cannot build a model for that axiom unless --mbqi is used. With --arrays-exp alone, every satisfiable query therefore ends in unknown, and CBMC reports VERIFICATION ERROR instead of VERIFICATION FAILED with a trace. Because all properties share one check-sat, the unknown also affects every other property in that query. Reproducer:

int main()
{
  void *p[4];
  __CPROVER_array_set(p, (void *)0);
  unsigned i;
  __CPROVER_assume(i < 4);
  __CPROVER_assert(p[i] != 0, "fails");
  return 0;
}

cbmc --cvc5 gives VERIFICATION FAILED on develop (826c1c7) and VERIFICATION ERROR with this PR. This holds with cvc5 1.3.4 both with #9287 applied and through a cvc5 --arrays-exp wrapper.

This matters in practice because the DFCC contracts library zero-initialises its object sets with __CPROVER_allocate(nof_objects * sizeof(void *), 1) (__CPROVER_contracts_obj_set_create_indexed_by_object_id / ..._append). I regenerated the cvc5 encodings for all CBMC proofs of mlkem-native and mldsa-native (405 proofs, LP64) with develop and with this PR. 36 of them change, and in 35 of those the only change is this single array_of(NULL) turning into a forall. Unsat run times stay the same, but any of these proofs that fails would now report an error instead of a counterexample.

Fix. Admit pointer constants and correct the comment:

-  // a literal converts to a value; a pointer constant (an object/offset
-  // encoding) or a compound term does not
+  // a literal (including a pointer constant, which convert_constant prints
+  // as a bit-vector literal) converts to a value; a compound term (e.g., an
+  // address_of or a typecast) does not
   return what.is_constant() &&
          (what.type().id() == ID_bool || what.type().id() == ID_signedbv ||
           what.type().id() == ID_unsignedbv || what.type().id() == ID_bv ||
           what.type().id() == ID_c_bool || what.type().id() == ID_c_enum_tag ||
-          what.type().id() == ID_floatbv);
+          what.type().id() == ID_floatbv || what.type().id() == ID_pointer);

I checked this change on top of 503d670:

• The reproducer reports VERIFICATION FAILED again.
• regression/cbmc/smt2_cvc5_as_const_value still passes.
• I regenerated all 405 encodings. In the 35 proofs above the output is again identical to develop. The only remaining difference from develop is the intended new handling when a bit-vector is converted back to an array (attempt_signature_generation, which cvc5 could not parse before this PR).

It would be good to add the reproducer above as a regression test (--cvc5, expecting ^VERIFICATION FAILED$).

Related limitation, not a regression. A non-literal what, e.g. __CPROVER_array_set(p, (void *)16), reaches the solver as the typecast ((_ sign_extend 32) (_ bv16 32)). It still gets the forall, and cvc5 then answers unknown for all properties, including the ones that hold. Before this PR the same input was a cvc5 parse error, so nothing gets worse. It may still be worth checking whether simplifying what first would fold such casts into constants that as const can use.