--- src/solvers/qbf/qbf_bdd_core.cpp.orig	2018-12-18 13:04:16.000000000 -0700
+++ src/solvers/qbf/qbf_bdd_core.cpp	2019-01-31 20:32:20.731352424 -0700
@@ -13,6 +13,7 @@ Author: CM Wintersteiger
 #include <util/arith_tools.h>
 #include <util/invariant.h>
 #include <util/std_expr.h>
+#include <util/expr_util.h>
 
 #include <cuddObj.hh> // CUDD Library
 
@@ -51,7 +52,7 @@ literalt qbf_bdd_certificatet::new_varia
   literalt l=qdimacs_coret::new_variable();
 
   if(!is_quantified(l))
-    add_quantifier(quantifiert::EXISTENTIAL, l);
+    add_quantifier(quantifiert::typet::EXISTENTIAL, l);
 
   return l;
 }
@@ -105,7 +106,7 @@ propt::resultt qbf_bdd_coret::prop_solve
   {
     unsigned var=it->var_no;
 
-    if(it->type==quantifiert::EXISTENTIAL)
+    if(it->type==quantifiert::typet::EXISTENTIAL)
     {
       #if 0
       std::cout << "BDD E: " << var << ", " <<
@@ -124,7 +125,7 @@ propt::resultt qbf_bdd_coret::prop_solve
     else
     {
       INVARIANT(
-        it->type == quantifiert::UNIVERSAL,
+        it->type == quantifiert::typet::UNIVERSAL,
         "only handles quantified variables");
       #if 0
       std::cout << "BDD A: " << var << ", " <<
@@ -138,15 +139,15 @@ propt::resultt qbf_bdd_coret::prop_solve
   if(*matrix==bdd_manager->bddOne())
   {
     compress_certificate();
-    return P_SATISFIABLE;
+    return resultt::P_SATISFIABLE;
   }
   else if(*matrix==bdd_manager->bddZero())
   {
     model_bdds.clear();
-    return P_UNSATISFIABLE;
+    return resultt::P_UNSATISFIABLE;
   }
   else
-    return P_ERROR;
+    return resultt::P_ERROR;
 }
 
 bool qbf_bdd_coret::is_in_core(literalt l) const
@@ -241,19 +242,19 @@ void qbf_bdd_coret::compress_certificate
 {
   status() << "Compressing Certificate" << eom;
 
-  for(const quantifiert &quantifier : quantifiers)
+  for(auto it=quantifiers.begin(); it!=quantifiers.end(); it++)
   {
-    if(quantifier.type==quantifiert::EXISTENTIAL)
+    if(it->type==quantifiert::typet::EXISTENTIAL)
     {
-      const BDD &var=*bdd_variable_map[quantifier.var_no];
-      const BDD &model=*model_bdds[quantifier.var_no];
+      const BDD &var=*bdd_variable_map[it->var_no];
+      const BDD &model=*model_bdds[it->var_no];
 
       if(model==bdd_manager->bddOne() ||
          model==bdd_manager->bddZero())
       {
-        for(const quantifiert &quantifier2 : quantifiers)
+        for(auto it2=it; it2!=quantifiers.end(); it2++)
         {
-          BDD &model2=*model_bdds[quantifier2.var_no];
+          BDD &model2=*model_bdds[it2->var_no];
 
           if(model==bdd_manager->bddZero())
             model2=model2.AndAbstract(~var, var);
@@ -272,7 +273,7 @@ const exprt qbf_bdd_certificatet::f_get(
     !find_quantifier(l, q), "no model for unquantified variables");
 
   // universal?
-  if(q.type==quantifiert::UNIVERSAL)
+  if(q.type==quantifiert::typet::UNIVERSAL)
   {
     INVARIANT(l.var_no() != 0, "input literal wasn't properly initialized");
     variable_mapt::const_iterator it=variable_map.find(l.var_no());
@@ -286,7 +287,7 @@ const exprt qbf_bdd_certificatet::f_get(
     extractbit_exprt extract_expr(sym, from_integer(index, integer_typet()));
 
     if(l.sign())
-      extract_expr.negate();
+      extract_expr = to_extractbit_expr(boolean_negate(extract_expr));
 
     return extract_expr;
   }
@@ -294,7 +295,7 @@ const exprt qbf_bdd_certificatet::f_get(
   {
     // skolem functions for existentials
     INVARIANT(
-      q.type == quantifiert::EXISTENTIAL,
+      q.type == quantifiert::typet::EXISTENTIAL,
       "only quantified literals are supported");
 
     function_cachet::const_iterator it=function_cache.find(l.var_no());
--- src/solvers/qbf/qbf_skizzo_core.cpp.orig	2019-01-17 19:58:21.060120367 -0700
+++ src/solvers/qbf/qbf_skizzo_core.cpp	2019-01-17 19:59:16.132962875 -0700
@@ -48,7 +48,7 @@ propt::resultt qbf_skizzo_coret::prop_so
 {
   // sKizzo crashes on empty instances
   if(no_clauses()==0)
-    return P_SATISFIABLE;
+    return resultt::P_SATISFIABLE;
 
   {
     std::string msg=
@@ -107,7 +107,7 @@ propt::resultt qbf_skizzo_coret::prop_so
     if(!result_found)
     {
       messaget::error() << "Skizzo failed: unknown result" << messaget::eom;
-      return P_ERROR;
+      return resultt::P_ERROR;
     }
   }
 
@@ -119,14 +119,14 @@ propt::resultt qbf_skizzo_coret::prop_so
     messaget::status() << "Skizzo: TRUE" << messaget::eom;
 
     if(get_certificate())
-      return P_ERROR;
+      return resultt::P_ERROR;
 
-    return P_SATISFIABLE;
+    return resultt::P_SATISFIABLE;
   }
   else
   {
     messaget::status() << "Skizzo: FALSE" << messaget::eom;
-    return P_UNSATISFIABLE;
+    return resultt::P_UNSATISFIABLE;
   }
 }
 
--- src/solvers/qbf/qbf_squolem_core.cpp.orig	2018-12-18 13:04:16.000000000 -0700
+++ src/solvers/qbf/qbf_squolem_core.cpp	2019-01-17 19:59:16.133962873 -0700
@@ -202,7 +202,7 @@ const exprt qbf_squolem_coret::f_get(lit
     extractbit_exprt extract_expr(sym, from_integer(index, integer_typet()));
 
     if(l.sign())
-      extract_expr.negate();
+      extract_expr = to_extractbit_expr(boolean_negate(extract_expr));
 
     return extract_expr;
   }