diff --git a/regression/contracts/function_apply_01/test.desc b/regression/contracts/function_apply_01/test.desc
index abc8686ad8e..4f37c84c808 100644
--- a/regression/contracts/function_apply_01/test.desc
+++ b/regression/contracts/function_apply_01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --apply-code-contracts
 ^EXIT=0$
@@ -6,4 +6,3 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Applying code contracts currently also checks them.
diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc
index d9a2ec0a8ca..a44b7e292f5 100644
--- a/regression/contracts/function_check_01/test.desc
+++ b/regression/contracts/function_check_01/test.desc
@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.
diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc
index db7ee5aa32a..1a229ae78d6 100644
--- a/regression/contracts/function_check_04/test.desc
+++ b/regression/contracts/function_check_04/test.desc
@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^\[main.assertion.1\] assertion x == 0: SUCCESS$
 ^\[foo.1\] : FAILURE$
 ^VERIFICATION FAILED$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.
diff --git a/regression/contracts/function_check_mem_01/main.c b/regression/contracts/function_check_mem_01/main.c
index b63364f4d57..10d79cf8190 100644
--- a/regression/contracts/function_check_mem_01/main.c
+++ b/regression/contracts/function_check_mem_01/main.c
@@ -33,7 +33,7 @@ void foo(bar *x)
   __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
 {
   x->x += 1;
-  return
+  return;
 }
 
 int main()
diff --git a/regression/contracts/function_check_mem_01/test.desc b/regression/contracts/function_check_mem_01/test.desc
index b46799f781b..c45406ad744 100644
--- a/regression/contracts/function_check_mem_01/test.desc
+++ b/regression/contracts/function_check_mem_01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --check-code-contracts
 ^EXIT=0$
diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc
index d9a2ec0a8ca..a44b7e292f5 100644
--- a/regression/contracts/invar_check_01/test.desc
+++ b/regression/contracts/invar_check_01/test.desc
@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.
diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc
index d9a2ec0a8ca..a44b7e292f5 100644
--- a/regression/contracts/invar_check_02/test.desc
+++ b/regression/contracts/invar_check_02/test.desc
@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.
diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc
index d9a2ec0a8ca..a44b7e292f5 100644
--- a/regression/contracts/invar_check_03/test.desc
+++ b/regression/contracts/invar_check_03/test.desc
@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.
diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc
index 7414b7f58a6..f24cdd9f7e4 100644
--- a/regression/contracts/invar_check_04/test.desc
+++ b/regression/contracts/invar_check_04/test.desc
@@ -1,12 +1,9 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^\[main.1\] Loop invariant violated before entry: SUCCESS$
 ^\[main.2\] Loop invariant not preserved: SUCCESS$
 ^\[main.assertion.1\] assertion r == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
index 98d0d1248eb..e5139b90da4 100644
--- a/src/goto-instrument/code_contracts.cpp
+++ b/src/goto-instrument/code_contracts.cpp
@@ -24,6 +24,8 @@ Date: February 2016
 
 #include "loop_utils.h"
 
+enum class contract_opst { APPLY, CHECK };
+
 class code_contractst
 {
 public:
@@ -32,21 +34,19 @@ class code_contractst
     goto_functionst &_goto_functions):
       ns(_symbol_table),
       symbol_table(_symbol_table),
-      goto_functions(_goto_functions),
-      temporary_counter(0)
+      goto_functions(_goto_functions)
   {
   }
 
-  void operator()();
+  void operator()(contract_opst op_type);
 
 protected:
   namespacet ns;
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
 
-  unsigned temporary_counter;
-
-  std::unordered_set<irep_idt> summarized;
+  void apply_code_contracts();
+  void check_code_contracts();
 
   void code_contracts(goto_functionst::goto_functiont &goto_function);
 
@@ -54,113 +54,28 @@ class code_contractst
     goto_programt &goto_program,
     goto_programt::targett target);
 
-  void add_contract_check(
-    const irep_idt &function,
+  void apply_invariant(
+    goto_functionst::goto_functiont &goto_function,
+    const local_may_aliast &local_may_alias,
+    const goto_programt::targett loop_head,
+    const loopt &loop);
+
+  void check_contract(
+    const irep_idt &function_id,
+    goto_functionst::goto_functiont &goto_function,
     goto_programt &dest);
 
+  void check_apply_invariant(
+    goto_functionst::goto_functiont &goto_function,
+    const local_may_aliast &local_may_alias,
+    const goto_programt::targett loop_head,
+    const loopt &loop);
+
   const symbolt &new_tmp_symbol(
     const typet &type,
     const source_locationt &source_location);
 };
 
-static void check_apply_invariants(
-  goto_functionst::goto_functiont &goto_function,
-  const local_may_aliast &local_may_alias,
-  const goto_programt::targett loop_head,
-  const loopt &loop)
-{
-  assert(!loop.empty());
-
-  // find the last back edge
-  goto_programt::targett loop_end=loop_head;
-  for(loopt::const_iterator
-      it=loop.begin();
-      it!=loop.end();
-      ++it)
-    if((*it)->is_goto() &&
-       (*it)->get_target()==loop_head &&
-       (*it)->location_number>loop_end->location_number)
-      loop_end=*it;
-
-  // see whether we have an invariant
-  exprt invariant=
-    static_cast<const exprt&>(
-      loop_end->guard.find(ID_C_spec_loop_invariant));
-  if(invariant.is_nil())
-    return;
-
-  // change H: loop; E: ...
-  // to
-  // H: assert(invariant);
-  // havoc;
-  // assume(invariant);
-  // if(guard) goto E:
-  // loop;
-  // assert(invariant);
-  // assume(false);
-  // E: ...
-
-  // find out what can get changed in the loop
-  modifiest modifies;
-  get_modifies(local_may_alias, loop, modifies);
-
-  // build the havocking code
-  goto_programt havoc_code;
-
-  // assert the invariant
-  {
-    goto_programt::targett a=havoc_code.add_instruction(ASSERT);
-    a->guard=invariant;
-    a->function=loop_head->function;
-    a->source_location=loop_head->source_location;
-    a->source_location.set_comment("Loop invariant violated before entry");
-  }
-
-  // havoc variables being written to
-  build_havoc_code(loop_head, modifies, havoc_code);
-
-  // assume the invariant
-  {
-    goto_programt::targett assume=havoc_code.add_instruction(ASSUME);
-    assume->guard=invariant;
-    assume->function=loop_head->function;
-    assume->source_location=loop_head->source_location;
-  }
-
-  // non-deterministically skip the loop if it is a do-while loop
-  if(!loop_head->is_goto())
-  {
-    goto_programt::targett jump=havoc_code.add_instruction(GOTO);
-    jump->guard=side_effect_expr_nondett(bool_typet());
-    jump->targets.push_back(loop_end);
-    jump->function=loop_head->function;
-    jump->source_location=loop_head->source_location;
-  }
-
-  // Now havoc at the loop head. Use insert_swap to
-  // preserve jumps to loop head.
-  goto_function.body.insert_before_swap(loop_head, havoc_code);
-
-  // assert the invariant at the end of the loop body
-  {
-    goto_programt::instructiont a(ASSERT);
-    a.guard=invariant;
-    a.function=loop_end->function;
-    a.source_location=loop_end->source_location;
-    a.source_location.set_comment("Loop invariant not preserved");
-    goto_function.body.insert_before_swap(loop_end, a);
-    ++loop_end;
-  }
-
-  // change the back edge into assume(false) or assume(guard)
-  loop_end->targets.clear();
-  loop_end->type=ASSUME;
-  if(loop_head->is_goto())
-    loop_end->guard.make_false();
-  else
-    loop_end->guard.make_not();
-}
-
 void code_contractst::apply_contract(
   goto_programt &goto_program,
   goto_programt::targett target)
@@ -175,14 +90,24 @@ void code_contractst::apply_contract(
   const symbolt &f_sym=ns.lookup(function);
   const code_typet &type=to_code_type(f_sym.type);
 
-  exprt requires=
+  exprt requires =
     static_cast<const exprt&>(type.find(ID_C_spec_requires));
-  exprt ensures=
+  exprt ensures =
     static_cast<const exprt&>(type.find(ID_C_spec_ensures));
 
-  // is there a contract?
   if(ensures.is_nil())
-    return;
+  {
+    // If there is no contract at all, we skip this function.
+    if(requires.is_nil())
+    {
+      return;
+    }
+    else
+    {
+      // If there's no ensures but is a requires, treat it as ensures(true)
+      ensures = true_exprt();
+    }
+  }
 
   // replace formal parameters by arguments, replace return
   replace_symbolt replace;
@@ -215,75 +140,131 @@ void code_contractst::apply_contract(
     goto_program.insert_before_swap(target, a);
     ++target;
   }
+  // TODO: Havoc write set of the function between assert and ensure.
 
   target->make_assumption(ensures);
-
-  summarized.insert(function);
 }
 
-void code_contractst::code_contracts(
-  goto_functionst::goto_functiont &goto_function)
+void code_contractst::apply_invariant(
+  goto_functionst::goto_functiont &goto_function,
+  const local_may_aliast &local_may_alias,
+  const goto_programt::targett loop_head,
+  const loopt &loop)
 {
-  local_may_aliast local_may_alias(goto_function);
-  natural_loops_mutablet natural_loops(goto_function.body);
-
-  // iterate over the (natural) loops in the function
-  for(natural_loops_mutablet::loop_mapt::const_iterator
-      l_it=natural_loops.loop_map.begin();
-      l_it!=natural_loops.loop_map.end();
-      l_it++)
-    check_apply_invariants(
-      goto_function,
-      local_may_alias,
-      l_it->first,
-      l_it->second);
-
-  // look at all function calls
-  Forall_goto_program_instructions(it, goto_function.body)
-    if(it->is_function_call())
-      apply_contract(goto_function.body, it);
-}
+  PRECONDITION(!loop.empty());
 
-const symbolt &code_contractst::new_tmp_symbol(
-  const typet &type,
-  const source_locationt &source_location)
-{
-  return get_fresh_aux_symbol(
-    type,
-    id2string(source_location.get_function()),
-    "tmp_cc",
-    source_location,
-    irep_idt(),
-    symbol_table);
+  // find the last back edge
+  goto_programt::targett loop_end=loop_head;
+  for(const goto_programt::targett &inst : loop)
+  {
+    if(inst->is_goto() &&
+       inst->get_target()==loop_head &&
+       inst->location_number>loop_end->location_number)
+    {
+      loop_end=inst;
+    }
+  }
+
+  exprt invariant = static_cast<const exprt&>(
+    loop_end->guard.find(ID_C_spec_loop_invariant));
+  if(invariant.is_nil())
+  {
+    return;
+  }
+
+  // TODO: Allow for not havocking in the for/while case
+
+  // change H: loop; E: ...
+  // to
+  // H: assert(invariant);
+  // havoc;
+  // assume(invariant);
+  // assume(!guard);
+  // E: ...
+
+  // find out what can get changed in the loop
+  modifiest modifies;
+  get_modifies(local_may_alias, loop, modifies);
+
+  // build the havocking code
+  goto_programt havoc_code;
+
+  // assert the invariant
+  {
+    goto_programt::targett a=havoc_code.add_instruction(ASSERT);
+    a->guard=invariant;
+    a->function=loop_head->function;
+    a->source_location=loop_head->source_location;
+    a->source_location.set_comment("Loop invariant violated before entry");
+  }
+
+  // havoc variables being written to
+  build_havoc_code(loop_head, modifies, havoc_code);
+
+  // assume the invariant
+  {
+    goto_programt::targett assume=havoc_code.add_instruction(ASSUME);
+    assume->guard=invariant;
+    assume->function=loop_head->function;
+    assume->source_location=loop_head->source_location;
+  }
+
+  // assume !guard
+  // TODO: consider breaks and how they're implemented.
+  // TODO: Also consider continues and whether they jump to loop end or head
+  {
+    goto_programt::targett assume = havoc_code.add_instruction(ASSUME);
+    if(loop_head->is_goto())
+    {
+      assume->guard = loop_head->guard;
+    }
+    else
+    {
+      assume->guard = loop_end->guard;
+      assume->guard.make_not();
+    }
+    assume->function = loop_head->function;
+    assume->source_location = loop_head->source_location;
+  }
+
+  // Clear out loop body
+  for(const goto_programt::targett &inst : loop)
+  {
+    inst->make_skip();
+  }
+
+  // Now havoc at the loop head. Use insert_swap to
+  // preserve jumps to loop head.
+  goto_function.body.insert_before_swap(loop_head, havoc_code);
+
+  // Remove all the skips we created.
+  remove_skip(goto_function.body);
 }
 
-void code_contractst::add_contract_check(
-  const irep_idt &function,
+void code_contractst::check_contract(
+  const irep_idt &function_id,
+  goto_functionst::goto_functiont &goto_function,
   goto_programt &dest)
 {
-  assert(!dest.instructions.empty());
-
-  goto_functionst::function_mapt::iterator f_it=
-    goto_functions.function_map.find(function);
-  assert(f_it!=goto_functions.function_map.end());
+  PRECONDITION(!dest.instructions.empty());
 
-  const goto_functionst::goto_functiont &gf=f_it->second;
+  exprt requires =
+    static_cast<const exprt&>(goto_function.type.find(ID_C_spec_requires));
+  exprt ensures =
+    static_cast<const exprt&>(goto_function.type.find(ID_C_spec_ensures));
 
-  const exprt &requires=
-    static_cast<const exprt&>(gf.type.find(ID_C_spec_requires));
-  const exprt &ensures=
-    static_cast<const exprt&>(gf.type.find(ID_C_spec_ensures));
-  assert(ensures.is_not_nil());
+  // Nothing to check if ensures is nil.
+  if(ensures.is_nil()) {
+    return;
+  }
 
   // build:
   // if(nondet)
   //   decl ret
   //   decl parameter1 ...
   //   assume(requires)  [optional]
-  //   ret=function(parameter1, ...)
+  //   ret = function(parameter1, ...)
   //   assert(ensures)
-  //   assume(false)
-  // skip: ...
 
   // build skip so that if(nondet) can refer to it
   goto_programt tmp_skip;
@@ -301,18 +282,20 @@ void code_contractst::add_contract_check(
 
   // prepare function call including all declarations
   code_function_callt call;
-  call.function()=ns.lookup(function).symbol_expr();
+  call.function()=ns.lookup(function_id).symbol_expr();
   replace_symbolt replace;
 
   // decl ret
-  if(gf.type.return_type()!=empty_typet())
+  // TODO: Handle void functions
+  // void functions seem to be handled by goto-cc
+  if(goto_function.type.return_type()!=empty_typet())
   {
     goto_programt::targett d=check.add_instruction(DECL);
     d->function=skip->function;
     d->source_location=skip->source_location;
 
     symbol_exprt r=
-      new_tmp_symbol(gf.type.return_type(),
+      new_tmp_symbol(goto_function.type.return_type(),
                      d->source_location).symbol_expr();
     d->code=code_declt(r);
 
@@ -322,24 +305,20 @@ void code_contractst::add_contract_check(
   }
 
   // decl parameter1 ...
-  for(code_typet::parameterst::const_iterator
-      p_it=gf.type.parameters().begin();
-      p_it!=gf.type.parameters().end();
-      ++p_it)
+  for(const auto &p_it : goto_function.type.parameters())
   {
     goto_programt::targett d=check.add_instruction(DECL);
     d->function=skip->function;
     d->source_location=skip->source_location;
 
     symbol_exprt p=
-      new_tmp_symbol(p_it->type(),
-                     d->source_location).symbol_expr();
+      new_tmp_symbol(p_it.type(), d->source_location).symbol_expr();
     d->code=code_declt(p);
 
     call.arguments().push_back(p);
 
-    if(!p_it->get_identifier().empty())
-      replace.insert(p_it->get_identifier(), p);
+    if(!p_it.get_identifier().empty())
+      replace.insert(p_it.get_identifier(), p);
   }
 
   // assume(requires)
@@ -369,28 +348,179 @@ void code_contractst::add_contract_check(
   // rewrite any use of __CPROVER_return_value
   replace(a->guard);
 
-  // assume(false)
-  goto_programt::targett af=check.add_instruction();
-  af->make_assumption(false_exprt());
-  af->function=skip->function;
-  af->source_location=ensures.source_location();
-
   // prepend the new code to dest
   check.destructive_append(tmp_skip);
   dest.destructive_insert(dest.instructions.begin(), check);
 }
 
-void code_contractst::operator()()
+void code_contractst::check_apply_invariant(
+  goto_functionst::goto_functiont &goto_function,
+  const local_may_aliast &local_may_alias,
+  const goto_programt::targett loop_head,
+  const loopt &loop)
+{
+  PRECONDITION(!loop.empty());
+
+  // find the last back edge
+  goto_programt::targett loop_end=loop_head;
+  for(const goto_programt::targett &inst : loop)
+    if(inst->is_goto() &&
+       inst->get_target()==loop_head &&
+       inst->location_number>loop_end->location_number)
+      loop_end=inst;
+
+  // see whether we have an invariant
+  exprt invariant=
+    static_cast<const exprt&>(
+      loop_end->guard.find(ID_C_spec_loop_invariant));
+  if(invariant.is_nil())
+    return;
+
+  // change H: loop; E: ...
+  // to
+  // H: assert(invariant);
+  // havoc writes of loop;
+  // assume(invariant);
+  // loop (minus the ending goto);
+  // assert(invariant);
+  // assume(!guard)
+  // E:
+  // ...
+
+  // find out what can get changed in the loop
+  modifiest modifies;
+  get_modifies(local_may_alias, loop, modifies);
+
+  // build the havocking code
+  goto_programt havoc_code;
+
+  // assert the invariant
+  {
+    goto_programt::targett a=havoc_code.add_instruction(ASSERT);
+    a->guard=invariant;
+    a->function=loop_head->function;
+    a->source_location=loop_head->source_location;
+    a->source_location.set_comment("Loop invariant violated before entry");
+  }
+
+  // havoc variables being written to
+  build_havoc_code(loop_head, modifies, havoc_code);
+
+  // assume the invariant
+  {
+    goto_programt::targett assume=havoc_code.add_instruction(ASSUME);
+    assume->guard=invariant;
+    assume->function=loop_head->function;
+    assume->source_location=loop_head->source_location;
+  }
+
+  // assert the invariant at the end of the loop body
+  {
+    goto_programt::instructiont a(ASSERT);
+    a.guard=invariant;
+    a.function=loop_end->function;
+    a.source_location=loop_end->source_location;
+    a.source_location.set_comment("Loop invariant not preserved");
+
+    goto_function.body.insert_before_swap(loop_end, a);
+    ++loop_end;
+  }
+
+  // change the back edge into assume(!guard)
+  loop_end->targets.clear();
+  loop_end->type=ASSUME;
+  if(loop_head->is_goto())
+  {
+    loop_end->guard = loop_head->guard;
+  }
+  else
+  {
+    loop_end->guard.make_not();
+  }
+
+  // Now havoc at the loop head. Use insert_swap to
+  // preserve jumps to loop head.
+  goto_function.body.insert_before_swap(loop_head, havoc_code);
+}
+
+const symbolt &code_contractst::new_tmp_symbol(
+  const typet &type,
+  const source_locationt &source_location)
+{
+  return get_fresh_aux_symbol(
+    type,
+    id2string(source_location.get_function()),
+    "tmp_cc",
+    source_location,
+    ID_C,
+    symbol_table);
+}
+
+void code_contractst::apply_code_contracts()
 {
   Forall_goto_functions(it, goto_functions)
-    code_contracts(it->second);
+  {
+    goto_functionst::goto_functiont &goto_function = it->second;
+
+    // TODO: This aliasing check is insufficiently strong, in general.
+    local_may_aliast local_may_alias(goto_function);
+    natural_loops_mutablet natural_loops(goto_function.body);
+
+    for(const auto &l_it : natural_loops.loop_map)
+    {
+      apply_invariant(goto_function,
+                      local_may_alias,
+                      l_it.first,
+                      l_it.second);
+    }
+
+    Forall_goto_program_instructions(it, goto_function.body)
+    {
+      if(it->is_function_call())
+      {
+        apply_contract(goto_function.body, it);
+      }
+    }
+  }
+
+  goto_functions.update();
+}
 
+void code_contractst::check_code_contracts()
+{
   goto_functionst::function_mapt::iterator i_it=
     goto_functions.function_map.find(INITIALIZE_FUNCTION);
-  assert(i_it!=goto_functions.function_map.end());
+  CHECK_RETURN(i_it!=goto_functions.function_map.end());
+
+  Forall_goto_functions(it, goto_functions)
+  {
+    goto_functionst::goto_functiont &goto_function = it->second;
+
+    // TODO: This aliasing check is insufficiently strong, in general.
+    local_may_aliast local_may_alias(goto_function);
+    natural_loops_mutablet natural_loops(goto_function.body);
+
+    for(const auto &l_it : natural_loops.loop_map)
+    {
+      check_apply_invariant(goto_function,
+                            local_may_alias,
+                            l_it.first,
+                            l_it.second);
+    }
+
+    Forall_goto_program_instructions(it, goto_function.body)
+    {
+      if(it->is_function_call())
+      {
+        apply_contract(goto_function.body, it);
+      }
+    }
+  }
 
-  for(const auto &contract : summarized)
-    add_contract_check(contract, i_it->second.body);
+  Forall_goto_functions(it, goto_functions)
+  {
+    check_contract(it->first, it->second, i_it->second.body);
+  }
 
   // remove skips
   remove_skip(i_it->second.body);
@@ -398,7 +528,27 @@ void code_contractst::operator()()
   goto_functions.update();
 }
 
-void code_contracts(goto_modelt &goto_model)
+void code_contractst::operator()(contract_opst op_type)
+{
+  switch(op_type)
+  {
+    case contract_opst::APPLY:
+      apply_code_contracts();
+      break;
+    case contract_opst::CHECK:
+      check_code_contracts();
+      break;
+  }
+}
+
+void check_code_contracts(goto_modelt &goto_model)
+{
+  code_contractst(goto_model.symbol_table, goto_model.goto_functions)
+    (contract_opst::CHECK);
+}
+
+void apply_code_contracts(goto_modelt &goto_model)
 {
-  code_contractst(goto_model.symbol_table, goto_model.goto_functions)();
+  code_contractst(goto_model.symbol_table, goto_model.goto_functions)
+    (contract_opst::APPLY);
 }
diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h
index dc02902c142..7c7c02c09c0 100644
--- a/src/goto-instrument/code_contracts.h
+++ b/src/goto-instrument/code_contracts.h
@@ -16,6 +16,7 @@ Date: February 2016
 
 class goto_modelt;
 
-void code_contracts(goto_modelt &);
+void apply_code_contracts(goto_modelt &);
+void check_code_contracts(goto_modelt &);
 
 #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 4582509df7d..6f629b46463 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1046,11 +1046,18 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     goto_model.goto_functions.update();
   }
 
-  // verify and set invariants and pre/post-condition pairs
+  // Uses (without checking) invariants and pre/post-condition pairs.
   if(cmdline.isset("apply-code-contracts"))
   {
     status() << "Applying Code Contracts" << eom;
-    code_contracts(goto_model);
+    apply_code_contracts(goto_model);
+  }
+
+  // Uses invariants and pre/post-condition pairs and verifies that they hold.
+  if(cmdline.isset("check-code-contracts"))
+  {
+    status() << "Checking Code Contracts" << eom;
+    check_code_contracts(goto_model);
   }
 
   // replace function pointers, if explicitly requested
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index 706083df63e..d8286c53c74 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -87,8 +87,8 @@ Author: Daniel Kroening, kroening@kroening.com
   "(interpreter)(show-reaching-definitions)" \
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
-  "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
-  "(show-threaded)(list-calls-args)" \
+  "(horn)(skip-loops):(apply-code-contracts)(check-code-contracts)" \
+  "(model-argc-argv):(show-threaded)(list-calls-args)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
   OPT_AGGRESSIVE_SLICER \