Direct CVC4 to use ALL logics

This changes CVC4 to use ALL logics when solving. This has the
advantages that:
1. We will no longer receive errors when quantified expressions
   are sent to CVC4.
2. We may now solve more problems.
The disadvantages are:
A. Solving may take longer in some cases when quantifiers are
   not used.
B. CVC4 can now (more easily?) report "unknown".
Note that due to introducing quantifiers in expressions in
prior commits/work, reporting of unknown is now handled and can
be achieved with z3 already.

Author: TGWDB

src/solvers/smt2/smt2_conv.cpp

@@ -96,6 +96,7 @@ smt2_convt::smt2_convt(
     break;
 
   case solvert::CVC4:
+    logic = "ALL";
     use_array_of_bool = true;
     use_as_const = true;
     break;