remove encoding of arrays of bools into bitvector

[kroening]

The encoding of arrays of booleans as arrays of (_ bitvec 1) was necessary
when solvers did not support arrays of booleans.

This support is now broadly available, removing the need for this code path.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a 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).
• 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.

[codecov]

Codecov Report

Merging #6206 (475a878) into develop (3d16d64) will decrease coverage by 0.00%.
The diff coverage is 88.88%.

@@             Coverage Diff             @@
##           develop    #6206      +/-   ##
===========================================
- Coverage    76.81%   76.81%   -0.01%     
===========================================
  Files         1582     1582              
  Lines       182776   182750      -26     
===========================================
- Hits        140405   140378      -27     
- Misses       42371    42372       +1     

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.h	100.00% <ø> (ø)
src/solvers/smt2/smt2_conv.cpp	67.48% <88.88%> (-0.13%)	⬇️
src/goto-checker/solver_factory.cpp	73.33% <0.00%> (-2.67%)	⬇️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 5469136...475a878. Read the comment docs.

[martin-cs]

I remember this being a MathSAT thing. Have you checked if they now support it?

[TGWDB]

I remember this being a MathSAT thing. Have you checked if they now support it?

Sadly this looks true.

$ ./mathsat -version
MathSAT5 version 5.6.6 (218275631c24) (Apr 23 2021 07:55:22, gmp 6.1.2, gcc 7.5.0, 64-bit)
$ ./mathsat ~/github/testing/Issue5977/z3-latest.smt2
(error "Arrays with Bool as argument are not supported")
$ grep Array ~/github/testing/Issue5977/z3-latest.smt2 | grep Bool
(define-fun |__CPROVER_threads_exited#1| () (Array (_ BitVec 64) Bool) ((as const (Array (_ BitVec 64) Bool)) false))

[martin-cs]

Yeah... IIRC it was because MathSAT has a strong separation between terms and formulae and so you can't have a formula-level proposition appearing in a term-level sort / expression. Formally they are correct but it is a bit of a pain and one of the reasons why the foundations of SMT-LIB 3 are changing.

[TGWDB]

Is there interest in updating this PR to include special handling for MathSAT? Even if @kroening is not interested in doing the change, if the end result is desirable I don't mind picking up from here and adding a special case for MathSAT to this code.