Freeze property literal for incremental analysis

MiniSAT melts assumed literals that were not explicitly frozen before. Therefore
checking two equal properties could result in the property literal being
eliminated if the solver was run with different assumptions between the two
checks.

src/ebmc/ebmc_base.cpp

@@ -134,7 +134,8 @@ int ebmc_baset::finish_bmc(prop_conv_solvert &solver) {
       disjuncts.push_back(literal_exprt(!l));
 
     auto converted_or = solver.convert(disjunction(disjuncts));
-    solver.push({literal_exprt{converted_or}});
+    solver.push({literal_exprt(converted_or)});
+    solver.set_frozen(converted_or);
 
     decision_proceduret::resultt dec_result=
       solver.dec_solve();