diff --git a/regression/cbmc-cover/branch3/test.desc b/regression/cbmc-cover/branch3/test.desc
index 057b9d56a31..9226cc75866 100644
--- a/regression/cbmc-cover/branch3/test.desc
+++ b/regression/cbmc-cover/branch3/test.desc
@@ -3,6 +3,7 @@ main.c
 --cover branch --unwind 6
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* .* of .* covered \(100.0%\)$
+^\*\* .* of .* covered \(.*\)$
 --
 ^warning: ignoring
+^\[main.coverage.*\] file main.c line .* function main block .* branch .*: FAILED$
diff --git a/regression/cbmc-cover/built-ins1/main.c b/regression/cbmc-cover/built-ins1/main.c
index 2822ea8e7b2..dceca3a443b 100644
--- a/regression/cbmc-cover/built-ins1/main.c
+++ b/regression/cbmc-cover/built-ins1/main.c
@@ -1,9 +1,11 @@
+#include <string.h>
+
 int main()
 {
   char a[10];
   __CPROVER_input("a[3]", a[3]);
 
-  int len = strlen(a);
+  int len=strlen(a);
 
   if(len==3)
   {
@@ -13,5 +15,6 @@ int main()
   {
     return -1;
   }
+
   return 1;
 }
diff --git a/regression/cbmc-cover/built-ins1/test.desc b/regression/cbmc-cover/built-ins1/test.desc
index 49b517629f3..d80a20e49ef 100644
--- a/regression/cbmc-cover/built-ins1/test.desc
+++ b/regression/cbmc-cover/built-ins1/test.desc
@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 4 of 7 covered
+^\*\* 5 of 8 covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-
diff --git a/regression/cbmc-cover/built-ins3/main.c b/regression/cbmc-cover/built-ins3/main.c
index 5d89d3dd2c8..8c2f79e49b7 100644
--- a/regression/cbmc-cover/built-ins3/main.c
+++ b/regression/cbmc-cover/built-ins3/main.c
@@ -5,6 +5,8 @@ int main()
   const char *s="test";
   int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
 
+  __CPROVER_input("return value puts", ret);
+
   if(ret<0)
   {
     return 1;
diff --git a/regression/cbmc-cover/built-ins3/test.desc b/regression/cbmc-cover/built-ins3/test.desc
index bd3fc9fdaa3..ec3829bc662 100644
--- a/regression/cbmc-cover/built-ins3/test.desc
+++ b/regression/cbmc-cover/built-ins3/test.desc
@@ -3,7 +3,7 @@ main.c
 --cover location --unwind 10
 ^EXIT=0$
 ^SIGNAL=0$
-^\*\* 4 of 4 covered
+^\*\* 5 of .* covered
 --
 ^warning: ignoring
 ^\[.*<builtin-library-
diff --git a/regression/cbmc-cover/built-ins4/main.c b/regression/cbmc-cover/built-ins4/main.c
index 2822ea8e7b2..06ea031a2e4 100644
--- a/regression/cbmc-cover/built-ins4/main.c
+++ b/regression/cbmc-cover/built-ins4/main.c
@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];
diff --git a/regression/cbmc-cover/built-ins5/main.c b/regression/cbmc-cover/built-ins5/main.c
index 2822ea8e7b2..06ea031a2e4 100644
--- a/regression/cbmc-cover/built-ins5/main.c
+++ b/regression/cbmc-cover/built-ins5/main.c
@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];
diff --git a/regression/cbmc-cover/built-ins6/main.c b/regression/cbmc-cover/built-ins6/main.c
index 2822ea8e7b2..06ea031a2e4 100644
--- a/regression/cbmc-cover/built-ins6/main.c
+++ b/regression/cbmc-cover/built-ins6/main.c
@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];
diff --git a/regression/cbmc-cover/built-ins7/main.c b/regression/cbmc-cover/built-ins7/main.c
index 2822ea8e7b2..06ea031a2e4 100644
--- a/regression/cbmc-cover/built-ins7/main.c
+++ b/regression/cbmc-cover/built-ins7/main.c
@@ -1,3 +1,5 @@
+#include <string.h>
+
 int main()
 {
   char a[10];
diff --git a/regression/cbmc-cover/inlining1/main.c b/regression/cbmc-cover/inlining1/main.c
index c15b715bc76..ac37bc65f27 100644
--- a/regression/cbmc-cover/inlining1/main.c
+++ b/regression/cbmc-cover/inlining1/main.c
@@ -1,3 +1,5 @@
+// Discussion point: is the branch below one goal or two?
+
 inline void my_func(int x)
 {
   if(x)
diff --git a/regression/cbmc-cover/inlining1/test.desc b/regression/cbmc-cover/inlining1/test.desc
index 1c2f5cff9fb..a0447a39469 100644
--- a/regression/cbmc-cover/inlining1/test.desc
+++ b/regression/cbmc-cover/inlining1/test.desc
@@ -3,9 +3,9 @@ main.c
 --cover branch
 ^EXIT=0$
 ^SIGNAL=0$
-^\[my_func.coverage.1\] file main.c line 3 function my_func block 1 branch false: SATISFIED$
-^\[my_func.coverage.2\] file main.c line 3 function my_func block 1 branch true: FAILED$
-^\[my_func.coverage.3\] file main.c line 3 function my_func block 2 branch false: FAILED$
-^\[my_func.coverage.4\] file main.c line 3 function my_func block 2 branch true: SATISFIED$
+^\[main.coverage.1\] file main.c line 15 function main entry point: SATISFIED$
+^\[my_func.coverage.1\] file main.c line 5 function my_func entry point: SATISFIED$
+^\[my_func.coverage.2\] file main.c line 5 function my_func block 1 branch false: SATISFIED$
+^\[my_func.coverage.3\] file main.c line 5 function my_func block 1 branch true: SATISFIED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Free2/test.desc b/regression/cbmc/Free2/test.desc
index 950f6791fef..caab5ef644d 100644
--- a/regression/cbmc/Free2/test.desc
+++ b/regression/cbmc/Free2/test.desc
@@ -1,8 +1,10 @@
 CORE
 main.c
---pointer-check
+
 ^EXIT=10$
 ^SIGNAL=0$
+^.*free argument must be dynamic object: FAILURE$
+^.*free argument has offset zero: SUCCESS$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index aa1d82e0102..6cfe07b0e2c 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -112,6 +112,8 @@ void ansi_c_internal_additions(std::string &code)
     "void __VERIFIER_assume(__CPROVER_bool assumption);\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     "void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    "void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);\n"
     "__CPROVER_bool __CPROVER_equal();\n"
     "__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n"
     "__CPROVER_bool __CPROVER_invalid_pointer(const void *);\n"
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 251bb828b6f..94da717f33d 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -19,6 +19,7 @@ extern const void *__CPROVER_memory_leak;
 
 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
+void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
 
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index 493c9a74ef8..b0c9c1f3e6c 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -145,14 +145,13 @@ inline void free(void *ptr)
 {
   __CPROVER_HIDE:;
   // If ptr is NULL, no operation is performed.
+  __CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
+                         "free argument must be dynamic object");
+  __CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0,
+                         "free argument has offset zero");
+
   if(ptr!=0)
   {
-    // is it dynamic?
-    __CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),
-                     "free argument is dynamic object");
-    __CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0,
-                     "free argument has offset zero");
-
     // catch double free
     if(__CPROVER_deallocated==ptr)
       __CPROVER_assert(0, "double free");
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
index c0ad5465c6a..bc772e59608 100644
--- a/src/cbmc/bmc_cover.cpp
+++ b/src/cbmc/bmc_cover.cpp
@@ -204,8 +204,6 @@ bool bmc_covert::operator()()
   // This maps property IDs to 'goalt'
   forall_goto_functions(f_it, goto_functions)
   {
-    // Functions are already inlined.
-    if(f_it->second.is_inlined()) continue;
     forall_goto_program_instructions(i_it, f_it->second.body)
     {
       if(i_it->is_assert())
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 265759fc698..aa2736cb862 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/convert_nondet.h>
 #include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/link_to_library.h>
@@ -780,9 +781,8 @@ bool cbmc_parse_optionst::process_goto_program(
 
     mm_io(goto_model);
 
-    // do partial inlining
-    status() << "Partial Inlining" << eom;
-    goto_partial_inline(goto_model, get_message_handler());
+    // instrument library preconditions
+    instrument_preconditions(goto_model);
 
     // remove returns, gcc vectors, complex
     remove_returns(goto_model);
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 397dfc10536..90dc6240b77 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -259,7 +259,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-value-sets"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
 
       // recalculate numbers, etc.
       goto_model.goto_functions.update();
@@ -275,7 +274,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-global-may-alias"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       do_remove_returns();
       parameter_assignments(goto_model);
 
@@ -292,7 +290,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-local-bitvector-analysis"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       parameter_assignments(goto_model);
 
       // recalculate numbers, etc.
@@ -316,7 +313,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-custom-bitvector-analysis"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       do_remove_returns();
       parameter_assignments(goto_model);
 
@@ -341,7 +337,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-escape-analysis"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       do_remove_returns();
       parameter_assignments(goto_model);
 
@@ -358,7 +353,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("custom-bitvector-analysis"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
       do_remove_returns();
       parameter_assignments(goto_model);
 
@@ -388,7 +382,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-points-to"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
 
       // recalculate numbers, etc.
       goto_model.goto_functions.update();
@@ -405,7 +398,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-intervals"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
 
       // recalculate numbers, etc.
       goto_model.goto_functions.update();
@@ -434,7 +426,6 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("list-calls-args"))
     {
       do_indirect_call_and_rtti_removal();
-      do_partial_inlining();
 
       list_calls_and_arguments(goto_model);
 
@@ -448,7 +439,6 @@ int goto_instrument_parse_optionst::doit()
       if(!cmdline.isset("inline"))
       {
         do_indirect_call_and_rtti_removal();
-        do_partial_inlining();
 
         // recalculate numbers, etc.
         goto_model.goto_functions.update();
@@ -977,8 +967,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("show-custom-bitvector-analysis") ||
      cmdline.isset("custom-bitvector-analysis"))
   {
-    do_partial_inlining();
-
     status() << "Propagating Constants" << eom;
     constant_propagator_ait constant_propagator_ai(goto_model);
     remove_skip(goto_model);
@@ -987,7 +975,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("escape-analysis"))
   {
     do_indirect_call_and_rtti_removal();
-    do_partial_inlining();
     do_remove_returns();
     parameter_assignments(goto_model);
 
@@ -1082,9 +1069,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("partial-inline"))
   {
     do_indirect_call_and_rtti_removal();
-
-    status() << "Partial inlining" << eom;
-    goto_partial_inline(goto_model, get_message_handler(), true);
+    do_partial_inlining();
 
     goto_model.goto_functions.update();
     goto_model.goto_functions.compute_loop_numbers();
@@ -1172,7 +1157,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
      cmdline.isset("concurrency"))
   {
     do_indirect_call_and_rtti_removal();
-    do_partial_inlining();
 
     status() << "Pointer Analysis" << eom;
     value_set_analysist value_set_analysis(ns);
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index 4da25537292..2474a7d7e8b 100644
--- a/src/goto-programs/Makefile
+++ b/src/goto-programs/Makefile
@@ -23,6 +23,7 @@ SRC = basic_blocks.cpp \
       goto_program_template.cpp \
       goto_trace.cpp \
       graphml_witness.cpp \
+      instrument_preconditions.cpp \
       interpreter.cpp \
       interpreter_evaluate.cpp \
       json_goto_trace.cpp \
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index f1a103e2428..fbf77309efe 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -1113,7 +1113,8 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
   }
-  else if(identifier==CPROVER_PREFIX "assert")
+  else if(identifier==CPROVER_PREFIX "assert" ||
+          identifier==CPROVER_PREFIX "precondition")
   {
     if(arguments.size()!=2)
     {
@@ -1123,16 +1124,28 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
+    bool is_precondition=
+      identifier==CPROVER_PREFIX "precondition";
+
     const irep_idt description=
       get_string_constant(arguments[1]);
 
     goto_programt::targett t=dest.add_instruction(ASSERT);
     t->guard=arguments[0];
     t->source_location=function.source_location();
-    t->source_location.set(
-      "user-provided",
-      !function.source_location().is_built_in());
-    t->source_location.set_property_class(ID_assertion);
+
+    if(is_precondition)
+    {
+      t->source_location.set_property_class(ID_precondition);
+    }
+    else
+    {
+      t->source_location.set(
+        "user-provided",
+        !function.source_location().is_built_in());
+      t->source_location.set_property_class(ID_assertion);
+    }
+
     t->source_location.set_comment(description);
 
     // let's double-check the type of the argument
diff --git a/src/goto-programs/instrument_preconditions.cpp b/src/goto-programs/instrument_preconditions.cpp
new file mode 100644
index 00000000000..f3d020ddad9
--- /dev/null
+++ b/src/goto-programs/instrument_preconditions.cpp
@@ -0,0 +1,148 @@
+/*******************************************************************\
+
+Module: Move preconditions of a function
+        to the call-site of the function
+
+Author: Daniel Kroening
+
+Date:   September 2017
+
+\*******************************************************************/
+
+#include "instrument_preconditions.h"
+
+#include <util/replace_symbol.h>
+
+std::vector<goto_programt::const_targett> get_preconditions(
+  const symbol_exprt &function,
+  const goto_functionst &goto_functions)
+{
+  const irep_idt &identifier=function.get_identifier();
+
+  auto f_it=goto_functions.function_map.find(identifier);
+  if(f_it==goto_functions.function_map.end())
+    return {};
+
+  const auto &body=f_it->second.body;
+
+  std::vector<goto_programt::const_targett> result;
+
+  for(auto i_it=body.instructions.begin();
+      i_it!=body.instructions.end();
+      i_it++)
+  {
+    if(i_it->is_location() ||
+       i_it->is_skip())
+      continue; // ignore
+
+    if(i_it->is_assert() &&
+       i_it->source_location.get_property_class()==ID_precondition)
+      result.push_back(i_it);
+    else
+      break; // preconditions must be at the front
+  }
+
+  return result;
+}
+
+void remove_preconditions(goto_programt &goto_program)
+{
+  for(auto &instruction : goto_program.instructions)
+  {
+    if(instruction.is_location() ||
+       instruction.is_skip())
+      continue; // ignore
+
+    if(instruction.is_assert() &&
+       instruction.source_location.get_property_class()==ID_precondition)
+      instruction.type=LOCATION;
+    else
+      break; // preconditions must be at the front
+  }
+}
+
+replace_symbolt actuals_replace_map(
+  const code_function_callt &call,
+  const namespacet &ns)
+{
+  PRECONDITION(call.function().id()==ID_symbol);
+  const symbolt &s=ns.lookup(to_symbol_expr(call.function()));
+  const auto &code_type=to_code_type(s.type);
+  const auto &parameters=code_type.parameters();
+  const auto &arguments=call.arguments();
+
+  replace_symbolt result;
+  std::size_t count=0;
+  for(const auto &p : parameters)
+  {
+    if(p.get_identifier()!=irep_idt() &&
+       arguments.size()>count)
+    {
+      exprt a=arguments[count];
+      if(a.type()!=p.type())
+        a=typecast_exprt(a, p.type());
+      symbol_exprt s(p.get_identifier(), p.type());
+      result.insert(s, a);
+    }
+    count++;
+  }
+
+  return result;
+}
+
+void instrument_preconditions(
+  const goto_modelt &goto_model,
+  goto_programt &goto_program)
+{
+  const namespacet ns(goto_model.symbol_table);
+
+  for(auto it=goto_program.instructions.begin();
+      it!=goto_program.instructions.end();
+      it++)
+  {
+    if(it->is_function_call())
+    {
+      // does the function we call have preconditions?
+      const auto &call=to_code_function_call(it->code);
+
+      if(call.function().id()==ID_symbol)
+      {
+        auto preconditions=
+          get_preconditions(to_symbol_expr(call.function()),
+                            goto_model.goto_functions);
+
+        source_locationt source_location=it->source_location;
+        irep_idt function=it->function;
+
+        replace_symbolt r=actuals_replace_map(call, ns);
+
+        // add before the call, with location of the call
+        for(const auto &p : preconditions)
+        {
+          goto_program.insert_before_swap(it);
+          exprt instance=p->guard;
+          r(instance);
+          it->make_assertion(instance);
+          it->function=function;
+          it->source_location=source_location;
+          it->source_location.set_property_class(ID_precondition_instance);
+          it->source_location.set_comment(p->source_location.get_comment());
+          it++;
+        }
+      }
+    }
+  }
+}
+
+void instrument_preconditions(goto_modelt &goto_model)
+{
+  // add at call site
+  for(auto &f_it : goto_model.goto_functions.function_map)
+    instrument_preconditions(
+      goto_model,
+      f_it.second.body);
+
+  // now remove the preconditions
+  for(auto &f_it : goto_model.goto_functions.function_map)
+    remove_preconditions(f_it.second.body);
+}
diff --git a/src/goto-programs/instrument_preconditions.h b/src/goto-programs/instrument_preconditions.h
new file mode 100644
index 00000000000..b73d10965e2
--- /dev/null
+++ b/src/goto-programs/instrument_preconditions.h
@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module: Move preconditions of a function
+        to the call-site of the function
+
+Author: Daniel Kroening
+
+Date:   September 2017
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
+#define CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
+
+#include <goto-programs/goto_model.h>
+
+void instrument_preconditions(goto_modelt &);
+
+#endif // CPROVER_GOTO_PROGRAMS_INSTRUMENT_PRECONDITIONS_H
diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp
index 5861d8d2fda..43c9ea9107c 100644
--- a/src/goto-programs/set_properties.cpp
+++ b/src/goto-programs/set_properties.cpp
@@ -122,8 +122,7 @@ void label_properties(goto_functionst &goto_functions)
       it=goto_functions.function_map.begin();
       it!=goto_functions.function_map.end();
       it++)
-    if(!it->second.is_inlined())
-      label_properties(it->second.body, property_counters);
+    label_properties(it->second.body, property_counters);
 }
 
 void make_assertions_false(goto_modelt &goto_model)
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 92457c747f3..cb8e1c89dd3 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -90,6 +90,8 @@ IREP_ID_ONE(assign_bitor)
 IREP_ID_ONE(assume)
 IREP_ID_ONE(assert)
 IREP_ID_ONE(assertion)
+IREP_ID_ONE(precondition)
+IREP_ID_ONE(precondition_instance)
 IREP_ID_ONE(goto)
 IREP_ID_ONE(gcc_computed_goto)
 IREP_ID_ONE(ifthenelse)