avoid incomplete constructor for or_exprt

An incompletely constructed or_exprt is avoided by using the
::disjunction(...) function instead.

Author: kroening

src/ebmc/ebmc_base.cpp

@@ -126,13 +126,14 @@ int ebmc_baset::finish_bmc(prop_conv_solvert &solver) {
       continue;
 
     status() << "Checking " << property.name << eom;
-    
-    or_exprt or_expr;
-    
+
+    or_exprt::operandst disjuncts;
+    disjuncts.reserve(property.timeframe_literals.size());
+
     for(auto l : property.timeframe_literals)
-      or_expr.operands().push_back(literal_exprt(!l));
+      disjuncts.push_back(literal_exprt(!l));
 
-    auto converted_or = solver.convert(or_expr);
+    auto converted_or = solver.convert(disjunction(disjuncts));
     solver.push({literal_exprt{converted_or}});
 
     decision_proceduret::resultt dec_result=