Merge pull request #4723 from smowton/smowton/fix/ool-decision-procedure-text

Out-of-line prop_conv_solvert::decision_procedure_text to work around g++-5 bug

Author: smowton

src/solvers/prop/prop_conv_solver.cpp

@@ -574,3 +574,13 @@ void prop_conv_solvert::pop()
 
   prop.set_assumptions(assumption_stack);
 }
+
+// This method out-of-line because gcc-5.5.0-12ubuntu1 20171010 miscompiles it
+// when inline (in certain build configurations, notably -O2 -g0) by producing
+// a non-virtual thunk with c++03 ABI but a function body with c++11 ABI, the
+// mismatch leading to a missing vtable entry and consequent null-pointer deref
+// whenever this function is called.
+std::string prop_conv_solvert::decision_procedure_text() const
+{
+  return "propositional reduction";
+}

src/solvers/prop/prop_conv_solver.h

@@ -39,10 +39,7 @@ class prop_conv_solvert : public conflict_providert,
   // overloading from decision_proceduret
   decision_proceduret::resultt dec_solve() override;
   void print_assignment(std::ostream &out) const override;
-  std::string decision_procedure_text() const override
-  {
-    return "propositional reduction";
-  }
+  std::string decision_procedure_text() const override;
   exprt get(const exprt &expr) const override;
 
   tvt l_get(literalt a) const override