diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index 68cfdb1e903..0a9d3406c15 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/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";
+}
diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h
index 0bb5dfe6adf..8bd6a728aaa 100644
--- a/src/solvers/prop/prop_conv_solver.h
+++ b/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