diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index 870590d8ffc..f311b35931d 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -37,7 +37,6 @@ SRC = adjust_float_expressions.cpp \
       parameter_assignments.cpp \
       pointer_arithmetic.cpp \
       printf_formatter.cpp \
-      property_checker.cpp \
       read_bin_goto_object.cpp \
       read_goto_binary.cpp \
       rebuild_goto_start_function.cpp \
diff --git a/src/goto-programs/property_checker.cpp b/src/goto-programs/property_checker.cpp
deleted file mode 100644
index 11ff035bb22..00000000000
--- a/src/goto-programs/property_checker.cpp
+++ /dev/null
@@ -1,60 +0,0 @@
-/*******************************************************************\
-
-Module: Property Checker Interface
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Property Checker Interface
-
-#include "property_checker.h"
-
-std::string property_checkert::as_string(resultt result)
-{
-  switch(result)
-  {
-  case property_checkert::resultt::PASS: return "OK";
-  case property_checkert::resultt::FAIL: return "FAILURE";
-  case property_checkert::resultt::ERROR: return "ERROR";
-  case property_checkert::resultt::UNKNOWN: return "UNKNOWN";
-  }
-
-  UNREACHABLE;
-}
-
-property_checkert::property_checkert(
-  message_handlert &_message_handler):
-  messaget(_message_handler)
-{
-}
-
-void property_checkert::initialize_property_map(const goto_modelt &goto_model)
-{
-  const namespacet ns(goto_model.symbol_table);
-
-  forall_goto_functions(it, goto_model.goto_functions)
-  {
-    if(
-      !to_code_type(ns.lookup(it->first).type).get_inlined() ||
-      it->first == goto_functionst::entry_point())
-    {
-      const goto_programt &goto_program=it->second.body;
-
-      forall_goto_program_instructions(i_it, goto_program)
-      {
-        if(!i_it->is_assert())
-          continue;
-
-        const source_locationt &source_location=i_it->source_location;
-
-        irep_idt property_id=source_location.get_property_id();
-
-        property_statust &property_status=property_map[property_id];
-        property_status.result=resultt::UNKNOWN;
-        property_status.location=i_it;
-      }
-    }
-  }
-}
diff --git a/src/goto-programs/property_checker.h b/src/goto-programs/property_checker.h
deleted file mode 100644
index 6b747709260..00000000000
--- a/src/goto-programs/property_checker.h
+++ /dev/null
@@ -1,55 +0,0 @@
-/*******************************************************************\
-
-Module: Property Checker Interface
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-/// \file
-/// Property Checker Interface
-
-#ifndef CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
-#define CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H
-
-// this is just an interface -- it won't actually do any checking!
-
-#include <util/message.h>
-
-#include "goto_trace.h"
-#include "goto_model.h"
-
-class property_checkert:public messaget
-{
-public:
-  property_checkert()
-  {
-  }
-
-  explicit property_checkert(
-    message_handlert &_message_handler);
-
-  enum class resultt { PASS, FAIL, ERROR, UNKNOWN };
-
-  static std::string as_string(resultt);
-
-  // Check whether all properties in goto_functions hold.
-  virtual resultt operator()(const goto_modelt &)=0;
-
-  struct property_statust
-  {
-    // this is the counterexample
-    goto_tracet error_trace;
-    resultt result;
-    goto_programt::const_targett location;
-  };
-
-  // the irep_idt is the property id
-  typedef std::map<irep_idt, property_statust> property_mapt;
-  property_mapt property_map;
-
-protected:
-  void initialize_property_map(const goto_modelt &);
-};
-
-#endif // CPROVER_GOTO_PROGRAMS_PROPERTY_CHECKER_H