diff --git a/regression/Makefile b/regression/Makefile
index 71e3494e073..0cfcb721aae 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -6,6 +6,9 @@ DIRS = ansi-c \
        goto-analyzer \
        goto-instrument \
        goto-instrument-typedef \
+       cbmc-incr-oneloop \
+       cbmc-incr \
+       cbmc-with-incr \
        test-script \
        # Empty last line
 
@@ -19,3 +22,4 @@ clean:
 			$(MAKE) -C "$$dir" clean; \
 		fi; \
 	done;
+
diff --git a/regression/array-refinement-with-incr/Array_UF9/main.c b/regression/array-refinement-with-incr/Array_UF9/main.c
index dcf6f7346f3..93cdba8bd31 100644
--- a/regression/array-refinement-with-incr/Array_UF9/main.c
+++ b/regression/array-refinement-with-incr/Array_UF9/main.c
@@ -11,7 +11,7 @@ unsigned int SIZE;
 int linear_search(int *a, int n, int q) {
   unsigned int j=0;
   while (j<n && a[j]!=q) {
-  j;
+  j++;
   if (j==20) j=-1;
   }
   if (j<SIZE) return 1;
diff --git a/regression/cbmc-incr-oneloop/Makefile b/regression/cbmc-incr-oneloop/Makefile
index 00c5ea25db4..c699f3a2837 100644
--- a/regression/cbmc-incr-oneloop/Makefile
+++ b/regression/cbmc-incr-oneloop/Makefile
@@ -1,11 +1,16 @@
 default: tests.log
 
 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
+	@if ! ../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula" ; then \
+	../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 tests.log: ../test.pl
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
-
+	@if ! ../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula" ; then \
+	../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 show:
 	@for dir in *; do \
 		if [ -d "$$dir" ]; then \
diff --git a/regression/cbmc-incr-oneloop/unwind-forever1/test.desc b/regression/cbmc-incr-oneloop/unwind-forever1/test.desc
index 5d03502707e..15abdc45fac 100644
--- a/regression/cbmc-incr-oneloop/unwind-forever1/test.desc
+++ b/regression/cbmc-incr-oneloop/unwind-forever1/test.desc
@@ -1,4 +1,4 @@
-CORE
+THOROUGH
 main.c
  --incremental-check main.0
 ^EXIT=142$
diff --git a/regression/cbmc-incr-oneloop/unwind-forever2/test.desc b/regression/cbmc-incr-oneloop/unwind-forever2/test.desc
index 920f3890da5..2d756f31228 100644
--- a/regression/cbmc-incr-oneloop/unwind-forever2/test.desc
+++ b/regression/cbmc-incr-oneloop/unwind-forever2/test.desc
@@ -1,4 +1,4 @@
-CORE
+THOROUGH
 main.c
 --incremental-check main.0
 ^EXIT=142$
diff --git a/regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc b/regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc
index 330d653e34c..b72857b7d7f 100644
--- a/regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc
+++ b/regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind-max 10 --incremental-check main.0
+--unwind-max 10 --incremental-check main.0 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-incr/Makefile b/regression/cbmc-incr/Makefile
index 08b694ea9b5..3c7ea145d38 100644
--- a/regression/cbmc-incr/Makefile
+++ b/regression/cbmc-incr/Makefile
@@ -1,13 +1,17 @@
 default: tests.log
 
-PARAM = --incremental --magic-numbers
+PARAM = --incremental 
 # --refine   --slice-formula
 
 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc $(PARAM)"
+	@if ! ../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --incremental" ; then \
+	../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 tests.log: ../test.pl
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc $(PARAM)"
+	@if ! ../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --incremental" ; then \
+	../failed-tests-printer.pl ; \
 
 show:
 	@for dir in *; do \
diff --git a/regression/cbmc-incr/unwinding-assertion1/test.desc b/regression/cbmc-incr/unwinding-assertion1/test.desc
index 3ede5ed0f72..901082308b7 100644
--- a/regression/cbmc-incr/unwinding-assertion1/test.desc
+++ b/regression/cbmc-incr/unwinding-assertion1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind-max 10
+--unwind-max 10 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-with-incr/Free1/test.desc b/regression/cbmc-with-incr/Free1/test.desc
index 02f1049518a..1b942c82d5f 100644
--- a/regression/cbmc-with-incr/Free1/test.desc
+++ b/regression/cbmc-with-incr/Free1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^Counterexample:$
diff --git a/regression/cbmc-with-incr/Free2/test.desc b/regression/cbmc-with-incr/Free2/test.desc
index 02f1049518a..1b942c82d5f 100644
--- a/regression/cbmc-with-incr/Free2/test.desc
+++ b/regression/cbmc-with-incr/Free2/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^Counterexample:$
diff --git a/regression/cbmc-with-incr/Free3/test.desc b/regression/cbmc-with-incr/Free3/test.desc
index fd1b888b81d..eabe12ba077 100644
--- a/regression/cbmc-with-incr/Free3/test.desc
+++ b/regression/cbmc-with-incr/Free3/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-with-incr/Free4/test.desc b/regression/cbmc-with-incr/Free4/test.desc
index fd1b888b81d..eabe12ba077 100644
--- a/regression/cbmc-with-incr/Free4/test.desc
+++ b/regression/cbmc-with-incr/Free4/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-with-incr/Function5/test.desc b/regression/cbmc-with-incr/Function5/test.desc
index 50371f73fff..3813c5fb2e7 100644
--- a/regression/cbmc-with-incr/Function5/test.desc
+++ b/regression/cbmc-with-incr/Function5/test.desc
@@ -1,10 +1,10 @@
 CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --stop-on-fail
 ^SIGNAL=0$
 ^EXIT=10$
 ^Counterexample:$
-^  dereference failure: object bounds in .*$
+^  dereference failure: pointer outside object bounds in .*$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
index d8033224594..68d47b3eac3 100644
--- a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
+++ b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
@@ -3,8 +3,8 @@ main.c
 --unwind-max 3 --no-unwinding-assertions --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.1\] assertion matriz\[\(signed long int\)j\]\[\(signed long int\)k\] <= maior: OK$
-^\[main\.assertion\.2\] assertion matriz\[\(signed long int\)0\]\[\(signed long int\)0\] < maior: FAILED$
+
+^\[main\.assertion\.2\] assertion matriz\[\(signed long int\)0\]\[\(signed long int\)0\] \< maior: FAILURE$
 ^\*\* 1 of 2 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Overflow_Addition1/test.desc b/regression/cbmc-with-incr/Overflow_Addition1/test.desc
index 5dbaca0c795..19990f58b06 100644
--- a/regression/cbmc-with-incr/Overflow_Addition1/test.desc
+++ b/regression/cbmc-with-incr/Overflow_Addition1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---signed-overflow-check
+--signed-overflow-check --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic5/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic5/test.desc
index 73810cf4375..9c7aa8bff15 100644
--- a/regression/cbmc-with-incr/Pointer_Arithmetic5/test.desc
+++ b/regression/cbmc-with-incr/Pointer_Arithmetic5/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check --bounds-check --function f
+--pointer-check --bounds-check --function f --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-with-incr/Pointer_Arithmetic8/test.desc b/regression/cbmc-with-incr/Pointer_Arithmetic8/test.desc
index 0f0f5660f42..4f863e7055e 100644
--- a/regression/cbmc-with-incr/Pointer_Arithmetic8/test.desc
+++ b/regression/cbmc-with-incr/Pointer_Arithmetic8/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
index cf4a284351e..65839c362ea 100644
--- a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
+++ b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
@@ -3,7 +3,7 @@ main.c
 --all-properties --little-endian
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.2\] .*: FAILED$
+^\[main\.assertion\.2\] .*: FAILURE$
 ^\*\* 1 of 2 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
index b2bf0ea5879..66cd2d31510 100644
--- a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
+++ b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
@@ -3,7 +3,7 @@ main.c
 --all-properties --bounds-check --32
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+array\.List dynamic object upper bound in p->List\[2\]: FAILURE
+\*\* 1 of 11 failed \(2 iterations\)
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
index a2ae3807cab..be32cac87b7 100644
--- a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
+++ b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
@@ -3,7 +3,7 @@ main.c
 --all-properties --bounds-check --32 --no-simplify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+^\[main\.array_bounds\.5\] array.List upper bound: FAILURE$
+^\*\* 1 of 9 failed (2 iterations)$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/String2/test.desc b/regression/cbmc-with-incr/String2/test.desc
index 75352ab9ea5..6ea447bc697 100644
--- a/regression/cbmc-with-incr/String2/test.desc
+++ b/regression/cbmc-with-incr/String2/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^Counterexample:$
diff --git a/regression/cbmc-with-incr/Undefined_Function1/test.desc b/regression/cbmc-with-incr/Undefined_Function1/test.desc
index d29ea2fc36e..f84df0453aa 100644
--- a/regression/cbmc-with-incr/Undefined_Function1/test.desc
+++ b/regression/cbmc-with-incr/Undefined_Function1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--stop-on-fail
 ^SIGNAL=0$
 ^\*\*\*\* WARNING: no body for function f$
 ^Counterexample:$
diff --git a/regression/cbmc-with-incr/pipe1/test.desc b/regression/cbmc-with-incr/pipe1/test.desc
index 95e607f531d..c24f5e9bf17 100644
--- a/regression/cbmc-with-incr/pipe1/test.desc
+++ b/regression/cbmc-with-incr/pipe1/test.desc
@@ -3,7 +3,7 @@ main.c
 --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.4\] assertion data\[1\]==31: FAILED$
+^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$
 ^\*\* 1 of 5 failed \(2 iterations\)$
 --
 ^warning: ignoring
diff --git a/scripts/reformat_docs.py b/scripts/reformat_docs.py
index eadc5359052..35dc6e12809 100644
--- a/scripts/reformat_docs.py
+++ b/scripts/reformat_docs.py
@@ -95,10 +95,6 @@ def is_block_valid(self, block):
     def convert_sections(self, block):
         return [self.format_module(block)]
 
-    def needs_new_header(self, file_contents):
-        return (re.search(r'^\/\/\/ \\file$', file_contents, flags=re.MULTILINE)
-                is None)
-
 
 class FunctionFormatter(GenericFormatter):
     def __init__(self, doc_width):
@@ -192,7 +188,6 @@ def convert_sections(self, block):
 
 def replace_block(
         block_contents,
-        file_contents,
         file,
         header_formatter,
         class_formatter,
@@ -204,10 +199,9 @@ def replace_block(
             {f.name: f.contents for f in parse_fields(block_contents.group(1))})
 
     if header_formatter.is_block_valid(block):
-        converted = header_formatter.convert(header_from_block(block))
-        if header_formatter.needs_new_header(file_contents) and converted:
-            return block_contents.group(0) + converted + '\n'
-        return block_contents.group(0)
+        return '%s%s\n' % (
+                block_contents.group(0),
+                header_formatter.convert(header_from_block(block)))
 
     if class_formatter.is_block_valid(block):
         return class_formatter.convert(class_from_block(block))
@@ -237,7 +231,6 @@ def convert_file(file, inplace):
     new_contents = block_re.sub(
             lambda match: replace_block(
                 match,
-                contents,
                 file,
                 header_formatter,
                 class_formatter,
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index dc0c469b64c..cee4cf420fe 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3166,7 +3166,6 @@ std::string expr2ct::convert_code_array_replace(
   unsigned indent)
 {
   std::string dest=indent_str(indent)+"ARRAY_REPLACE(";
-
   forall_operands(it, src)
   {
     unsigned p;
diff --git a/src/ansi-c/get-gcc-builtins.sh b/src/ansi-c/get-gcc-builtins.sh
index fd06b79945d..84175f0e293 100755
--- a/src/ansi-c/get-gcc-builtins.sh
+++ b/src/ansi-c/get-gcc-builtins.sh
@@ -25,7 +25,6 @@ cat > gcc-builtins.h <<EOF
 #include <unistd.h>
 #include <stdio.h>
 #include <wctype.h>
-
 typedef   char   __gcc_v8qi  __attribute__ ((__vector_size__ (8)));
 typedef   char   __gcc_v16qi __attribute__ ((__vector_size__ (16)));
 typedef   char   __gcc_v32qi __attribute__ ((__vector_size__ (32)));
@@ -50,7 +49,6 @@ typedef   long long __gcc_v2di __attribute__ ((__vector_size__ (16)));
 typedef   long long __gcc_v4di __attribute__ ((__vector_size__ (32)));
 typedef   long long __gcc_v8di __attribute__ ((__vector_size__ (64)));
 typedef   unsigned long long __gcc_di;
-
 EOF
 
 cat > builtins.h <<EOF
@@ -98,17 +96,14 @@ cat > builtins.h <<EOF
 #define short_unsigned_type_node unsigned short
 #define short_integer_type_node short
 #define unsigned_char_type_node unsigned char
-
 // some newer versions of GCC apparently support __floatXYZ
 #define dfloat32_type_node __float32
 #define dfloat64_type_node __float64
 #define dfloat128_type_node __float128
-
 #define build_qualified_type(t, q) q t
 #define build_pointer_type(t) t*
 #define TYPE_QUAL_VOLATILE volatile
 #define TYPE_QUAL_CONST const
-
 #define DEF_PRIMITIVE_TYPE(ENUM, TYPE) \
 NEXTDEF ENUM TYPE
 #define DEF_FUNCTION_TYPE_0(ENUM, RETURN) \
@@ -135,7 +130,6 @@ NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ARG8, A
 NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ARG8, ARG9, ARG10)
 #define DEF_FUNCTION_TYPE_11(ENUM, RETURN, ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ARG8, ARG9, ARG10, ARG11) \
 NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ARG8, ARG9, ARG10, ARG11)
-
 #define DEF_FUNCTION_TYPE_VAR_0(ENUM, RETURN) \
 NEXTDEF ENUM(name) RETURN name()
 #define DEF_FUNCTION_TYPE_VAR_1(ENUM, RETURN, ARG1) \
@@ -152,21 +146,15 @@ NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ...)
 NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ...)
 #define DEF_FUNCTION_TYPE_VAR_7(ENUM, RETURN, ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7) \
 NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ...)
-
 #define DEF_POINTER_TYPE(ENUM, TYPE) \
 NEXTDEF ENUM TYPE*
-
 #define DEF_POINTER_TYPE_CONST(ENUM, TYPE, C) \
 NEXTDEF ENUM const TYPE*
-
 #include "builtin-types.def"
-
 NEXTDEF DEF_BUILTIN(ENUM, NAME, CLASS, TYPE, LIBTYPE, BOTH_P, \
                   FALLBACK_P, NONANSI_P, ATTRS, IMPLICIT, COND) \
 TYPE(MANGLE(NAME));
-
 #include "i386-builtin-types-expanded.def"
-
 NEXTDEF BDESC(mask, icode, name, code, comparison, flag) \
 flag(MANGLEi386(name));
 NEXTDEF BDESC_FIRST(kind, KIND, mask, icode, name, code, comparison, flag) \
@@ -176,12 +164,10 @@ EOF
 grep '^DEF_VECTOR_TYPE' i386-builtin-types.def | \
   awk -F '[,() \t]' '{ print "#define " $3 " __gcc_" tolower($3) }' \
   > i386-builtin-types-expanded.def
-
 grep -v '^DEF_FUNCTION_TYPE[[:space:]]' i386-builtin-types.def | \
   grep '^DEF_P' | \
   sed '/^DEF_POINTER_TYPE[^,]*, [^,]*, [^,]*$/ s/_TYPE/_TYPE_CONST/' \
   >> i386-builtin-types-expanded.def
-
 cat i386-builtin-types.def | \
   sed '/^DEF_FUNCTION_TYPE[[:space:]]/! s/.*//' | \
   sed 's/^DEF_FUNCTION_TYPE[[:space:]]*(\([^,]*\))/\1_FTYPE_VOID/' | \
@@ -272,4 +258,4 @@ cat gcc-builtins.h | sed 's/__builtin/XX__builtin/' | \
   gcc -D__CPROVER_size_t=size_t -c -fno-builtin -x c - -o gcc-builtins.o
 rm gcc-builtins.o
 
-echo "Successfully built gcc-builtins.h"
+echo "Successfully built gcc-builtins.h"
\ No newline at end of file
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index 4d890b0b5fa..5e1d4880e64 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -1,6 +1,8 @@
 SRC = all_properties.cpp \
       bmc.cpp \
       bmc_cover.cpp \
+      bmc_incremental.cpp \
+      bmc_incremental_one_loop.cpp \
       bv_cbmc.cpp \
       cbmc_dimacs.cpp \
       cbmc_languages.cpp \
@@ -11,6 +13,8 @@ SRC = all_properties.cpp \
       fault_localization.cpp \
       show_vcc.cpp \
       symex_bmc.cpp \
+      symex_bmc_incremental.cpp \
+      symex_bmc_incremental_one_loop.cpp \
       symex_coverage.cpp \
       xml_interface.cpp \
       # Empty last line
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
index bd9c5242dd4..dffed8e6993 100644
--- a/src/cbmc/all_properties.cpp
+++ b/src/cbmc/all_properties.cpp
@@ -77,7 +77,8 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
       it!=bmc.equation.SSA_steps.end();
       it++)
   {
-    if(it->is_assert())
+    if(it->is_assert() &&
+       it->comment!=SYMEX_CONTINUATION_CHECK)
     {
       irep_idt property_id;
 
@@ -94,6 +95,9 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
       else
         continue;
 
+      // need to convert again as the context of the expression
+      //  may have changed
+      it->cond_literal=solver.convert(it->cond_expr);
       goal_map[property_id].instances.push_back(it);
     }
   }
@@ -102,6 +106,14 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   cover_goalst cover_goals(solver);
 
+  // set activation literal for incremental checking
+  cover_goals.activation_literal=bmc.equation.current_activation_literal();
+
+#if 0
+  std::cout << "cover_goals.activation_literal = "
+            << cover_goals.activation_literal << std::endl;
+#endif
+
   cover_goals.set_message_handler(get_message_handler());
   cover_goals.register_observer(*this);
 
@@ -117,6 +129,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   bool error=false;
 
+  solver.set_assumptions(bmc.equation.activate_assertions);
   decision_proceduret::resultt result=cover_goals();
 
   if(result==decision_proceduret::resultt::D_ERROR)
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index f92483d2441..02f6b6e0d71 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -49,6 +49,9 @@ void bmct::do_unwind_module()
 
 void bmct::error_trace()
 {
+  if(options.get_bool_option("stop-when-unsat"))
+    return;
+
   status() << "Building error trace" << eom;
 
   goto_tracet &goto_trace=safety_checkert::error_trace;
@@ -217,6 +220,65 @@ void bmct::report_failure()
   }
 }
 
+
+void bmct::slice()
+{
+  if(options.get_option("slice-by-trace")!="")
+  {
+    symex_slice_by_tracet symex_slice_by_trace(ns);
+
+    symex_slice_by_trace.slice_by_trace
+      (options.get_option("slice-by-trace"), equation);
+  }
+  // any properties to check at all?
+  if(equation.has_threads())
+  {
+    // we should build a thread-aware SSA slicer
+    statistics() << "no slicing due to threads" << eom;
+  }
+  else
+  {
+    if(options.get_bool_option("slice-formula"))
+    {
+      ::slice(equation);
+      statistics() << "slicing removed "
+                   << equation.count_ignored_SSA_steps()
+                   << " assignments" << eom;
+    }
+    else
+    {
+      if(options.get_list_option("cover").empty())
+      {
+        simple_slice(equation);
+        statistics() << "simple slicing removed "
+                     << equation.count_ignored_SSA_steps()
+                     << " assignments" << eom;
+      }
+    }
+  }
+  statistics() << "Generated " << symex().total_vccs
+               << " VCC(s), " << symex().remaining_vccs
+               << " remaining after simplification" << eom;
+}
+
+
+safety_checkert::resultt bmct::show(const goto_functionst &goto_functions)
+{
+  if(options.get_bool_option("show-vcc"))
+  {
+    show_vcc();
+    return safety_checkert::resultt::SAFE; // to indicate non-error
+  }
+
+  if(options.get_bool_option("program-only"))
+  {
+    show_program();
+    return safety_checkert::resultt::SAFE;
+  }
+
+  return safety_checkert::resultt::UNKNOWN;
+}
+
 void bmct::show_program()
 {
   unsigned count=1;
@@ -306,11 +368,10 @@ void bmct::show_program()
   }
 }
 
-safety_checkert::resultt bmct::run(
-  const goto_functionst &goto_functions)
+
+safety_checkert::resultt bmct::initialize()
 {
   const std::string mm=options.get_option("mm");
-  std::unique_ptr<memory_model_baset> memory_model;
 
   if(mm.empty() || mm=="sc")
     memory_model=std::unique_ptr<memory_model_baset>(new memory_model_sct(ns));
@@ -325,109 +386,62 @@ safety_checkert::resultt bmct::run(
     return safety_checkert::resultt::ERROR;
   }
 
-  symex.set_message_handler(get_message_handler());
-  symex.options=options;
+  symex().set_message_handler(get_message_handler());
+  symex().options=options;
 
   {
     const symbolt *init_symbol;
     if(!ns.lookup(CPROVER_PREFIX "initialize", init_symbol))
-      symex.language_mode=init_symbol->mode;
+      symex().language_mode=init_symbol->mode;
   }
 
   status() << "Starting Bounded Model Checking" << eom;
 
-  symex.last_source_location.make_nil();
+  symex().last_source_location.make_nil();
 
-  try
-  {
     // get unwinding info
     setup_unwind();
 
-    // perform symbolic execution
-    symex(goto_functions);
-
-    // add a partial ordering, if required
-    if(equation.has_threads())
-    {
-      memory_model->set_message_handler(get_message_handler());
-      (*memory_model)(equation);
-    }
-  }
+  return safety_checkert::resultt::UNKNOWN;
+}
 
-  catch(const std::string &error_str)
-  {
-    messaget message(get_message_handler());
-    message.error().source_location=symex.last_source_location;
-    message.error() << error_str << messaget::eom;
+/*******************************************************************\
 
-    return safety_checkert::resultt::ERROR;
-  }
+Function: bmct::step
 
-  catch(const char *error_str)
-  {
-    messaget message(get_message_handler());
-    message.error().source_location=symex.last_source_location;
-    message.error() << error_str << messaget::eom;
+  Inputs:
 
-    return safety_checkert::resultt::ERROR;
-  }
+ Outputs:
 
-  catch(std::bad_alloc)
-  {
-    error() << "Out of memory" << eom;
-    return safety_checkert::resultt::ERROR;
-  }
+ Purpose: do BMC
 
-  statistics() << "size of program expression: "
-               << equation.SSA_steps.size()
-               << " steps" << eom;
+\*******************************************************************/
 
+safety_checkert::resultt bmct::step(const goto_functionst &goto_functions)
+{
   try
   {
-    if(options.get_option("slice-by-trace")!="")
-    {
-      symex_slice_by_tracet symex_slice_by_trace(ns);
-
-      symex_slice_by_trace.slice_by_trace
-        (options.get_option("slice-by-trace"), equation);
-    }
+    // perform symbolic execution
+    symex()(goto_functions);
 
+    // add a partial ordering, if required
     if(equation.has_threads())
     {
-      // we should build a thread-aware SSA slicer
-      statistics() << "no slicing due to threads" << eom;
-    }
-    else
-    {
-      if(options.get_bool_option("slice-formula"))
-      {
-        slice(equation);
-        statistics() << "slicing removed "
-                     << equation.count_ignored_SSA_steps()
-                     << " assignments" << eom;
-      }
-      else
-      {
-        if(options.get_list_option("cover").empty())
-        {
-          simple_slice(equation);
-          statistics() << "simple slicing removed "
-                       << equation.count_ignored_SSA_steps()
-                       << " assignments" << eom;
-        }
-      }
+      memory_model->set_message_handler(get_message_handler());
+      (*memory_model)(equation);
     }
 
-    {
-      statistics() << "Generated " << symex.total_vccs
-                   << " VCC(s), " << symex.remaining_vccs
-                   << " remaining after simplification" << eom;
-    }
+  statistics() << "size of program expression: "
+               << equation.SSA_steps.size()
+               << " steps" << eom;
+
+  // perform slicing
+  slice();
 
     // coverage report
     std::string cov_out=options.get_option("symex-coverage-report");
     if(!cov_out.empty() &&
-       symex.output_coverage_report(goto_functions, cov_out))
+       symex().output_coverage_report(goto_functions, cov_out))
     {
       error() << "Failed to write symex coverage report" << eom;
       return safety_checkert::resultt::ERROR;
@@ -456,7 +470,7 @@ safety_checkert::resultt bmct::run(
 
     // any properties to check at all?
     if(!options.get_bool_option("program-only") &&
-       symex.remaining_vccs==0)
+     symex().remaining_vccs==0)
     {
       report_success();
       output_graphml(resultt::SAFE, goto_functions);
@@ -469,38 +483,48 @@ safety_checkert::resultt bmct::run(
       return safety_checkert::resultt::SAFE;
     }
 
-    return decide(goto_functions, prop_conv);
+  // do all properties
+  if(options.get_bool_option("stop-on-fail"))
+    return stop_on_fail(goto_functions, prop_conv);
+  else
+    return all_properties(goto_functions, prop_conv);
   }
-
   catch(std::string &error_str)
-  {
-    error() << error_str << eom;
-    return safety_checkert::resultt::ERROR;
-  }
+    {
+      messaget message(get_message_handler());
+      message.error().source_location=symex().last_source_location;
+      message.error() << error_str << messaget::eom;
+
+      return safety_checkert::resultt::ERROR;
+    }
+
+    catch(const char *error_str)
+    {
+      messaget message(get_message_handler());
+      message.error().source_location=symex().last_source_location;
+      message.error() << error_str << messaget::eom;
+
+      return safety_checkert::resultt::ERROR;
+    }
+
+    catch(std::bad_alloc)
+    {
+      error() << "Out of memory" << eom;
+      return safety_checkert::resultt::ERROR;
+    }
 
-  catch(const char *error_str)
-  {
-    error() << error_str << eom;
-    return safety_checkert::resultt::ERROR;
-  }
 
-  catch(std::bad_alloc)
-  {
-    error() << "Out of memory" << eom;
-    return safety_checkert::resultt::ERROR;
-  }
 }
 
-safety_checkert::resultt bmct::decide(
-  const goto_functionst &goto_functions,
-  prop_convt &prop_conv)
+
+safety_checkert::resultt bmct::run(
+  const goto_functionst &goto_functions)
 {
-  prop_conv.set_message_handler(get_message_handler());
+  safety_checkert::resultt result=initialize();
+  if(result!=safety_checkert::resultt::UNKNOWN)
+    return result;
 
-  if(options.get_bool_option("stop-on-fail"))
-    return stop_on_fail(goto_functions, prop_conv);
-  else
-    return all_properties(goto_functions, prop_conv);
+  return step(goto_functions);
 }
 
 safety_checkert::resultt bmct::stop_on_fail(
@@ -566,12 +590,12 @@ void bmct::setup_unwind()
       long uw=unsafe_string2int(val.substr(val.rfind(":")+1));
 
       if(thread_nr_set)
-        symex.set_unwind_thread_loop_limit(thread_nr, id, uw);
+        symex().set_unwind_thread_loop_limit(thread_nr, id, uw);
       else
-        symex.set_unwind_loop_limit(id, uw);
+        symex().set_unwind_loop_limit(id, uw);
     }
   }
 
   if(options.get_option("unwind")!="")
-    symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
+    symex().set_unwind_limit(options.get_unsigned_int_option("unwind"));
 }
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index e05a4de62f6..7a61ee19290 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <list>
 #include <map>
+#include <memory>
 
 #include <util/options.h>
 
@@ -26,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language_ui.h>
 #include <goto-symex/symex_target_equation.h>
 #include <goto-programs/safety_checker.h>
+#include <goto-symex/memory_model.h>
 
 #include "symex_bmc.h"
 
@@ -41,24 +43,30 @@ class bmct:public safety_checkert
     options(_options),
     ns(_symbol_table, new_symbol_table),
     equation(ns),
-    symex(ns, new_symbol_table, equation),
+    symex_ptr(new symex_bmct(ns, new_symbol_table, equation)),
     prop_conv(_prop_conv),
     ui(ui_message_handlert::uit::PLAIN)
   {
-    symex.constant_propagation=options.get_bool_option("propagation");
-    symex.record_coverage=
+    symex().constant_propagation=options.get_bool_option("propagation");
+    symex().record_coverage=
       !options.get_option("symex-coverage-report").empty();
   }
 
-  virtual resultt run(const goto_functionst &goto_functions);
   virtual ~bmct() { }
 
   // additional stuff
   expr_listt bmc_constraints;
 
+
   void set_ui(language_uit::uit _ui) { ui=_ui; }
+  friend class cbmc_satt;
+  friend class hw_cbmc_satt;
+  friend class counterexample_beautification_greedyt;
+
 
   // the safety_checkert interface
+  // ENHANCE: it would be reasonable to pass the goto_functions
+  //   parameter to the constructor
   virtual resultt operator()(
     const goto_functionst &goto_functions)
   {
@@ -66,12 +74,29 @@ class bmct:public safety_checkert
   }
 
 protected:
+  // for initialization of derived classes
+  bmct(
+    const optionst &_options,
+    const symbol_tablet &_symbol_table,
+    prop_convt& _prop_conv,
+    message_handlert &_message_handler):
+    safety_checkert(ns, _message_handler),
+    options(_options),
+    ns(_symbol_table, new_symbol_table),
+    equation(ns),
+    symex_ptr(NULL),
+    prop_conv(_prop_conv),
+    ui(ui_message_handlert::uit::PLAIN)
+  {
+  }
+
   const optionst &options;
   symbol_tablet new_symbol_table;
   namespacet ns;
   symex_target_equationt equation;
-  symex_bmct symex;
+  symex_bmct *symex_ptr;
   prop_convt &prop_conv;
+  std::unique_ptr<memory_model_baset> memory_model;
 
   // use gui format
   language_uit::uit ui;
@@ -79,15 +104,22 @@ class bmct:public safety_checkert
   virtual decision_proceduret::resultt
     run_decision_procedure(prop_convt &prop_conv);
 
-  virtual resultt decide(
-    const goto_functionst &,
-    prop_convt &);
-
   // unwinding
   virtual void setup_unwind();
   virtual void do_unwind_module();
   void do_conversion();
 
+  // run
+  virtual resultt run(const goto_functionst &goto_functions);
+
+  // decomposed run
+  virtual resultt initialize();
+  virtual resultt step(const goto_functionst &goto_functions);
+
+  // functions used in run
+  virtual void slice();
+  virtual resultt show(const goto_functionst &goto_functions);
+
   virtual void show_vcc();
   virtual void show_vcc_plain(std::ostream &out);
   virtual void show_vcc_json(std::ostream &out);
@@ -114,6 +146,14 @@ class bmct:public safety_checkert
   friend class bmc_all_propertiest;
   friend class bmc_covert;
   friend class fault_localizationt;
+
+private:
+  // We cannot use a reference member here
+  // because the initialization sequence would not be clean (Clang complains)
+  symex_bmct &symex()
+  {
+    return dynamic_cast<symex_bmct &>(*symex_ptr);
+  }
 };
 
 #endif // CPROVER_CBMC_BMC_H
diff --git a/src/cbmc/bmc_incremental.cpp b/src/cbmc/bmc_incremental.cpp
new file mode 100644
index 00000000000..a71dcc3d8f3
--- /dev/null
+++ b/src/cbmc/bmc_incremental.cpp
@@ -0,0 +1,166 @@
+/*******************************************************************\
+
+Module: Incremental Symbolic Execution of ANSI-C
+
+Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <limits>
+
+#include <goto-symex/slice.h>
+
+#include "bmc_incremental.h"
+
+/*******************************************************************\
+
+Function: bmc_incrementalt::step
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: run incremental BMC loop
+
+\*******************************************************************/
+
+safety_checkert::resultt bmc_incrementalt::step(
+  const goto_functionst &goto_functions)
+{
+  try
+  {
+    // We count only new assertions.
+    symex().total_vccs=0;
+    symex().remaining_vccs=0;
+
+    // perform symbolic execution
+    bool symex_done=
+      symex()(
+        symex_state,
+        goto_functions,
+        goto_functions.function_map.at(goto_functions.entry_point()).body);
+
+    // add a partial ordering, if required
+    if(equation.has_threads())
+    {
+      memory_model->set_message_handler(get_message_handler());
+      (*memory_model)(equation);
+    }
+
+    statistics() << "size of program expression: "
+                 << equation.SSA_steps.size()
+                 << " steps" << eom;
+
+    undo_slice(equation); // undo all previous slicings
+
+    slice();
+
+    resultt result=show(goto_functions);
+    if(result!=safety_checkert::resultt::UNKNOWN)
+      return result;
+
+    // any properties to check at all?
+    if(symex().remaining_vccs==0)
+    {
+      report_success();
+      result=safety_checkert::resultt::SAFE;
+    }
+    else
+    {
+      if(options.get_bool_option("stop-on-fail"))
+        result=stop_on_fail(goto_functions, prop_conv);
+      else
+        result=all_properties(goto_functions, prop_conv);
+    }
+
+    resultt term_cond=
+      options.get_bool_option("stop-when-unsat") ?
+        safety_checkert::resultt::UNSAFE : safety_checkert::resultt::SAFE;
+    return result==term_cond && !symex_done ?
+      safety_checkert::resultt::UNKNOWN : result;
+  }
+
+  catch(std::string &error_str)
+  {
+    error() << error_str << eom;
+    return safety_checkert::resultt::ERROR;
+  }
+
+  catch(const char *error_str)
+  {
+    error() << error_str << eom;
+    return safety_checkert::resultt::ERROR;
+  }
+
+  catch(std::bad_alloc)
+  {
+    error() << "Out of memory" << eom;
+    return safety_checkert::resultt::ERROR;
+  }
+}
+
+/*******************************************************************\
+
+Function: bmc_incrementalt::run
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: run incremental BMC loop
+
+\*******************************************************************/
+
+safety_checkert::resultt bmc_incrementalt::run(
+  const goto_functionst &goto_functions)
+{
+  safety_checkert::resultt result=initialize();
+  while(result==safety_checkert::resultt::UNKNOWN)
+  {
+    result=step();
+
+    // check unwinding assertions
+    if(result==safety_checkert::resultt::UNKNOWN &&
+       symex().add_loop_check())
+    {
+      resultt loop_check_result=
+        stop_on_fail(goto_functions, prop_conv);
+      bool earliest_loop_exit=
+        options.get_bool_option("earliest-loop-exit");
+      if(loop_check_result==safety_checkert::resultt::SAFE)
+        symex().update_loop_info(earliest_loop_exit ? false : true);
+      else if(loop_check_result==safety_checkert::resultt::UNSAFE)
+        symex().update_loop_info(earliest_loop_exit ? true : false);
+    }
+  }
+
+  return result;
+}
+
+/*******************************************************************\
+
+Function: bmc_incrementalt::setup_unwind
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void bmc_incrementalt::setup_unwind()
+{
+  bmct::setup_unwind();
+
+  if(options.get_option("unwind-min")!="")
+    symex().incr_min_unwind=options.get_unsigned_int_option("unwind-min");
+  if(options.get_option("unwind-max")!="")
+    symex().incr_max_unwind=options.get_unsigned_int_option("unwind-max");
+  else
+    symex().incr_max_unwind=std::numeric_limits<unsigned>::max();
+
+  status() << "Using incremental mode" << eom;
+  prop_conv.set_all_frozen();
+  equation.is_incremental=true;
+}
diff --git a/src/cbmc/bmc_incremental.h b/src/cbmc/bmc_incremental.h
new file mode 100644
index 00000000000..f4acd0542e1
--- /dev/null
+++ b/src/cbmc/bmc_incremental.h
@@ -0,0 +1,80 @@
+ /*******************************************************************\
+
+Module: Incremental Bounded Model Checking for ANSI-C  HDL
+
+Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
+
+ \*******************************************************************/
+
+#ifndef CPROVER_CBMC_BMC_INCREMENTAL_H
+#define CPROVER_CBMC_BMC_INCREMENTAL_H
+
+#include <list>
+#include <map>
+
+#include <util/options.h>
+
+#include <solvers/prop/prop_conv.h>
+#include <goto-symex/symex_target_equation.h>
+
+#include "symex_bmc_incremental.h"
+#include "bv_cbmc.h"
+#include "bmc.h"
+
+class bmc_incrementalt:public bmct
+{
+public:
+  bmc_incrementalt(
+    const optionst &_options,
+    const symbol_tablet &_symbol_table,
+    message_handlert &_message_handler,
+    prop_convt& _prop_conv,
+    const goto_functionst &_goto_functions):
+    bmct(
+      _options,
+      _symbol_table,
+      _prop_conv,
+      _message_handler),
+    goto_functions(_goto_functions)
+  {
+    symex_ptr=new symex_bmc_incrementalt(ns, new_symbol_table, equation);
+    symex().constant_propagation=options.get_bool_option("propagation");
+  }
+
+  virtual ~bmc_incrementalt() { }
+
+  // make public
+  virtual resultt run()
+  {
+    return run(goto_functions);
+  }
+  virtual resultt initialize()
+  {
+    return bmct::initialize();
+  }
+  virtual resultt step()
+  {
+    return step(goto_functions);
+  }
+
+protected:
+  const goto_functionst &goto_functions;
+
+  // ENHANCE: move this into symex_bmc
+  goto_symext::statet symex_state;
+
+  // overload
+  virtual resultt run(const goto_functionst &goto_functions);
+  virtual resultt step(const goto_functionst &goto_functions);
+
+  // unwinding
+  virtual void setup_unwind();
+
+ private:
+  symex_bmc_incrementalt &symex()
+  {
+    return dynamic_cast<symex_bmc_incrementalt &>(*symex_ptr);
+  }
+};
+
+#endif
diff --git a/src/cbmc/bmc_incremental_one_loop.cpp b/src/cbmc/bmc_incremental_one_loop.cpp
new file mode 100644
index 00000000000..a1ae74ffea5
--- /dev/null
+++ b/src/cbmc/bmc_incremental_one_loop.cpp
@@ -0,0 +1,156 @@
+/*******************************************************************\
+
+Module: Incremental Symbolic Execution of ANSI-C
+
+Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <goto-symex/slice.h>
+
+#include "bmc_incremental_one_loop.h"
+
+/*******************************************************************\
+
+Function: bmc_incremental_one_loopt::step
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: run incremental BMC loop
+
+ \*******************************************************************/
+
+safety_checkert::resultt bmc_incremental_one_loopt::step(
+  const goto_functionst &goto_functions)
+{
+  try
+  {
+    // We count only new assertions.
+    symex().total_vccs=0;
+    symex().remaining_vccs=0;
+
+    // perform symbolic execution
+    bool symex_done=
+      symex()(
+        symex_state, goto_functions,
+        goto_functions.function_map.at(goto_functions.entry_point()).body);
+
+    // add a partial ordering, if required
+    if(equation.has_threads())
+    {
+      memory_model->set_message_handler(get_message_handler());
+      (*memory_model)(equation);
+    }
+
+    statistics() << "size of program expression: "
+                 << equation.SSA_steps.size()
+                 << " steps" << eom;
+
+    undo_slice(equation); // undo all previous slicings
+
+    // perform slicing
+    slice();
+
+    // do diverse other options
+    {
+      resultt result=show(goto_functions);
+      if(result!=safety_checkert::resultt::UNKNOWN)
+        return result;
+    }
+
+    resultt result=safety_checkert::resultt::UNKNOWN;
+
+    // any properties to check at all?
+    if(symex().remaining_vccs==0)
+    {
+      report_success();
+      result=safety_checkert::resultt::SAFE;
+    }
+    else
+    {
+      if(options.get_bool_option("stop-on-fail"))
+        result=stop_on_fail(goto_functions, prop_conv);
+      else
+        result=all_properties(goto_functions, prop_conv);
+    }
+
+    resultt term_cond=
+      options.get_bool_option("stop-when-unsat") ?
+        safety_checkert::resultt::UNSAFE : safety_checkert::resultt::SAFE;
+    return result==term_cond && !symex_done ?
+      safety_checkert::resultt::UNKNOWN : result;
+  }
+
+  catch(std::string &error_str)
+  {
+    error() << error_str << eom;
+    return safety_checkert::resultt::ERROR;
+  }
+
+  catch(const char *error_str)
+  {
+    error() << error_str << eom;
+    return safety_checkert::resultt::ERROR;
+  }
+
+  catch(std::bad_alloc)
+  {
+    error() << "Out of memory" << eom;
+    return safety_checkert::resultt::ERROR;
+  }
+}
+
+/*******************************************************************\
+
+Function: bmc_incremental_one_loopt::run
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: run incremental BMC loop
+
+\*******************************************************************/
+
+safety_checkert::resultt bmc_incremental_one_loopt::run(
+  const goto_functionst &goto_functions)
+{
+  safety_checkert::resultt result=initialize();
+  while(result==safety_checkert::resultt::UNKNOWN)
+  {
+    result=step(goto_functions);
+  }
+
+  return result;
+}
+
+/*******************************************************************\
+
+Function: bmc_incremental_one_loopt::setup_unwind
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void bmc_incremental_one_loopt::setup_unwind()
+{
+  bmct::setup_unwind();
+
+  if(options.get_option("unwind-min")!="")
+    symex().incr_min_unwind=options.get_unsigned_int_option("unwind-min");
+  if(options.get_option("unwind-max")!="")
+    symex().incr_max_unwind=options.get_unsigned_int_option("unwind-max");
+  symex().ignore_assertions=(symex().incr_min_unwind>=2) &&
+    options.get_bool_option("ignore-assertions-before-unwind-min");
+  symex().incr_loop_id=options.get_option("incremental-check");
+
+  status() << "Using incremental mode" << eom;
+  prop_conv.set_all_frozen();
+  equation.is_incremental=true;
+}
diff --git a/src/cbmc/bmc_incremental_one_loop.h b/src/cbmc/bmc_incremental_one_loop.h
new file mode 100644
index 00000000000..988c5a8b1a3
--- /dev/null
+++ b/src/cbmc/bmc_incremental_one_loop.h
@@ -0,0 +1,73 @@
+/*******************************************************************\
+
+Module: Incremental Bounded Model Checking for ANSI-C  HDL
+
+Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_CBMC_BMC_INCREMENTAL_ONE_LOOP_H
+#define CPROVER_CBMC_BMC_INCREMENTAL_ONE_LOOP_H
+
+#include <list>
+#include <map>
+
+#include <util/options.h>
+#include <solvers/prop/prop_conv.h>
+#include <goto-symex/symex_target_equation.h>
+#include <goto-symex/memory_model.h>
+
+#include "symex_bmc_incremental_one_loop.h"
+#include "bv_cbmc.h"
+#include "bmc.h"
+
+
+class bmc_incremental_one_loopt:public bmct
+{
+public:
+  bmc_incremental_one_loopt(
+    const optionst &_options,
+    const symbol_tablet &_symbol_table,
+    message_handlert &_message_handler,
+    prop_convt& _prop_conv,
+    const goto_functionst &_goto_functions):
+    bmct(
+      _options,
+      _symbol_table,
+      _prop_conv,
+      _message_handler),
+    goto_functions(_goto_functions)
+  {
+    symex_ptr=new symex_bmc_incremental_one_loopt(
+      ns, new_symbol_table, equation, prop_conv);
+    symex().constant_propagation=options.get_bool_option("propagation");
+  }
+
+  virtual ~bmc_incremental_one_loopt() {}
+
+  // make public
+  virtual resultt run() { return run(goto_functions); }
+  virtual resultt initialize() { return bmct::initialize(); }
+  virtual resultt step() { return step(goto_functions); }
+
+protected:
+  const goto_functionst &goto_functions;
+
+  // ENHANCE: move this into symex_bmc
+  goto_symext::statet symex_state;
+
+  // overload
+  virtual resultt run(const goto_functionst &goto_functions);
+  virtual resultt step(const goto_functionst &goto_functions);
+
+  // unwinding
+  virtual void setup_unwind();
+
+private:
+  symex_bmc_incremental_one_loopt &symex()
+  {
+    return dynamic_cast<symex_bmc_incremental_one_loopt &>(*symex_ptr);
+  }
+};
+
+#endif
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index d2f1c178d8e..ee333f2aac0 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -1,9 +1,6 @@
 /*******************************************************************\
-
 Module: CBMC Command Line Option Processing
-
 Author: Daniel Kroening, kroening@kroening.com
-
 \*******************************************************************/
 
 /// \file
@@ -55,11 +52,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <pointer-analysis/add_failed_symbols.h>
 
+#include <analyses/goto_check.h>
+
 #include <langapi/mode.h>
 
 #include "cbmc_solvers.h"
 #include "cbmc_parse_options.h"
 #include "bmc.h"
+#include "bmc_incremental_one_loop.h"
+#include "bmc_incremental.h"
 #include "version.h"
 #include "xml_interface.h"
 
@@ -181,9 +182,18 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
       cmdline.get_value("localize-faults-method"));
   }
 
+  if(cmdline.isset("unwind-max"))
+    options.set_option("unwind-max", cmdline.get_value("unwind-max"));
+  if(cmdline.isset("unwind-min"))
+    options.set_option("unwind-min", cmdline.get_value("unwind-min"));
   if(cmdline.isset("unwind"))
     options.set_option("unwind", cmdline.get_value("unwind"));
 
+  if(cmdline.isset("ignore-assertions-before-unwind-min"))
+    options.set_option("ignore-assertions-before-unwind-min", true);
+  if(cmdline.isset("stop-when-unsat"))
+    options.set_option("stop-when-unsat", true);
+
   if(cmdline.isset("depth"))
     options.set_option("depth", cmdline.get_value("depth"));
 
@@ -196,6 +206,26 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.get_value("unwindset"));
 
+  if(cmdline.isset("incremental"))
+  {
+    options.set_option("refine", true);
+    options.set_option("refine-arrays", true);
+    options.set_option("incremental", true);
+  }
+  if(cmdline.isset("incremental-check"))
+  {
+    options.set_option("refine", true);
+    options.set_option("refine-arrays", true);
+    options.set_option(
+      "incremental-check", cmdline.get_value("incremental-check"));
+  }
+  if(cmdline.isset("earliest-loop-exit"))
+    options.set_option("earliest-loop-exit", true);
+
+  // heuristic unwinding numbers used for SV-COMP
+  if(cmdline.isset("magic-numbers"))
+    options.set_option("magic-numbers", true);
+
   // constant propagation
   if(cmdline.isset("no-propagation"))
     options.set_option("propagation", false);
@@ -420,6 +450,27 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
       cmdline.get_value("symex-coverage-report"));
 }
 
+bool cbmc_parse_optionst::options_exclusive(const char *opt1, const char *opt2)
+{
+  if(cmdline.isset(opt1) && cmdline.isset(opt2))
+  {
+    error() << "--" << opt1 << " cannot be used with --" << opt2 << eom;
+    return true;
+  }
+  return false;
+}
+
+
+bool cbmc_parse_optionst::options_inclusive(const char *opt1, const char *opt2)
+{
+  if(cmdline.isset(opt1) && !cmdline.isset(opt2))
+  {
+    error() << "--" << opt1 << " can only be used with --" << opt2 << eom;
+    return true;
+  }
+  return false;
+}
+
 /// invoke main modules
 int cbmc_parse_optionst::doit()
 {
@@ -457,6 +508,13 @@ int cbmc_parse_optionst::doit()
     return 1; // should contemplate EX_USAGE from sysexits.h
   }
 
+  if(options_exclusive("incremental", "unwind") ||
+     options_exclusive("incremental", "incremental-check") ||
+     options_inclusive("earliest-loop-exit", "incremental"))
+  {
+    return 1;
+  }
+
   register_languages();
 
   if(cmdline.isset("test-preprocessor"))
@@ -470,6 +528,38 @@ int cbmc_parse_optionst::doit()
 
   goto_functionst goto_functions;
 
+  // get solver
+  cbmc_solverst cbmc_solvers(options, symbol_table, ui_message_handler);
+  cbmc_solvers.set_ui(get_ui());
+
+  std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
+
+  try
+  {
+    cbmc_solver=cbmc_solvers.get_solver();
+  }
+
+  catch(const char *error_msg)
+  {
+    error() << error_msg << eom;
+    return 1; // should contemplate EX_SOFTWARE from sysexits.h
+  }
+
+  prop_convt &prop_conv=cbmc_solver->prop_conv();
+
+  std::unique_ptr<bmct> bmc;
+  if(options.get_option("incremental-check")!="")
+    bmc=std::unique_ptr<bmct>(
+      new bmc_incremental_one_loopt(
+        options, symbol_table, ui_message_handler, prop_conv, goto_functions));
+  else if(options.get_bool_option("incremental"))
+    bmc=std::unique_ptr<bmct>(
+      new bmc_incrementalt(
+        options, symbol_table, ui_message_handler, prop_conv, goto_functions));
+  else
+    bmc=std::unique_ptr<bmct>(
+      new bmct(options, symbol_table, ui_message_handler, prop_conv));
+
   expr_listt bmc_constraints;
 
   int get_goto_program_ret=
@@ -494,29 +584,8 @@ int cbmc_parse_optionst::doit()
   if(options.get_bool_option("java-unwind-enum-static"))
     remove_static_init_loops(symbol_table, goto_functions, options);
 
-  // get solver
-  cbmc_solverst cbmc_solvers(options, symbol_table, ui_message_handler);
-  cbmc_solvers.set_ui(get_ui());
-
-  std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
-
-  try
-  {
-    cbmc_solver=cbmc_solvers.get_solver();
-  }
-
-  catch(const char *error_msg)
-  {
-    error() << error_msg << eom;
-    return 1; // should contemplate EX_SOFTWARE from sysexits.h
-  }
-
-  prop_convt &prop_conv=cbmc_solver->prop_conv();
-
-  bmct bmc(options, symbol_table, ui_message_handler, prop_conv);
-
   // do actual BMC
-  return do_bmc(bmc, goto_functions);
+  return do_bmc(*bmc, goto_functions);
 }
 
 bool cbmc_parse_optionst::set_properties(goto_functionst &goto_functions)
@@ -928,7 +997,7 @@ int cbmc_parse_optionst::do_bmc(
   int result=6;
 
   // do actual BMC
-  switch(bmc.run(goto_functions))
+  switch(bmc(goto_functions))
   {
     case safety_checkert::resultt::SAFE:
       result=0;
@@ -939,6 +1008,9 @@ int cbmc_parse_optionst::do_bmc(
     case safety_checkert::resultt::ERROR:
       result=6;
       break;
+    case safety_checkert::resultt::UNKNOWN:
+     result=6;
+     break;
   }
 
   // let's log some more statistics
@@ -1051,6 +1123,17 @@ void cbmc_parse_optionst::help()
     " --unwind nr                  unwind nr times\n"
     " --unwindset L:B,...          unwind loop L with a bound of B\n"
     "                              (use --show-loops to get the loop IDs)\n"
+    " --incremental                check after each unwinding\n"
+    " --incremental-check L        check after each unwinding of loop L\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --unwind-min nr              start incremental check after nr unwindings\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --unwind-max nr              stop incremental check after nr unwindings\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --earliest-loop-exit         stop unwinding as soon as possible\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --ignore-assertions-before-unwind-min     only check loop assertions after loop unwound to unwind-min\n"
+    " --stop-when-unsat            for step case in k-induction checks\n"
     " --show-vcc                   show the verification conditions\n"
     " --slice-formula              remove assignments unrelated to property\n"
     " --unwinding-assertions       generate unwinding assertions\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index d95e60eb25b..50ba729eced 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -52,6 +52,10 @@ class optionst;
   "(nondet-static)" \
   "(version)" \
   "(cover):(symex-coverage-report):" \
+  "(incremental-check):(incremental)(earliest-loop-exit)" \
+  "(ignore-assertions-before-unwind-min)(stop-when-unsat)" \
+  "(unwind-max):(unwind-min):" \
+  "(magic-numbers)" \
   "(mm):" \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
   "(ppc-macos)(unsigned-char)" \
@@ -104,6 +108,9 @@ class cbmc_parse_optionst:
 
   void eval_verbosity();
 
+  bool options_exclusive(const char *opt1, const char *opt2);
+  bool options_inclusive(const char *opt1, const char *opt2);
+
   // get any additional stuff before finalizing the goto program
   virtual int get_modules(expr_listt &bmc_constraints)
   {
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
index 2beae26ff79..ae752bfce0f 100644
--- a/src/cbmc/fault_localization.cpp
+++ b/src/cbmc/fault_localization.cpp
@@ -229,7 +229,8 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
   return dec_result;
 }
 
-safety_checkert::resultt fault_localizationt::stop_on_fail()
+
+safety_checkert::resultt fault_localizationt::stop_on_fail(bool show_report)
 {
   switch(run_decision_procedure(bmc.prop_conv))
   {
diff --git a/src/cbmc/fault_localization.h b/src/cbmc/fault_localization.h
index 0c3ec090153..b4e3791351b 100644
--- a/src/cbmc/fault_localization.h
+++ b/src/cbmc/fault_localization.h
@@ -40,7 +40,7 @@ class fault_localizationt:
   }
 
   safety_checkert::resultt operator()();
-  safety_checkert::resultt stop_on_fail();
+  safety_checkert::resultt stop_on_fail(bool show_report=true);
 
   // override bmc_all_propertiest
   virtual void goal_covered(const cover_goalst::goalt &);
diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp
index ce6afc9dfa2..ba83ff20443 100644
--- a/src/cbmc/symex_bmc.cpp
+++ b/src/cbmc/symex_bmc.cpp
@@ -28,7 +28,7 @@ symex_bmct::symex_bmct(
 }
 
 /// show progress
-void symex_bmct::symex_step(
+bool symex_bmct::symex_step(
   const goto_functionst &goto_functions,
   statet &state)
 {
@@ -62,7 +62,7 @@ void symex_bmct::symex_step(
     statistics() << eom;
   }
 
-  goto_symext::symex_step(goto_functions, state);
+  bool symex_step_result =  goto_symext::symex_step(goto_functions, state);
 
   if(record_coverage &&
      // avoid an invalid iterator in state.source.pc
@@ -82,6 +82,7 @@ void symex_bmct::symex_step(
     else if(!state.guard.is_false())
       symex_coverage.covered(cur_pc, state.source.pc);
   }
+  return symex_step_result;
 }
 
 void symex_bmct::merge_goto(
diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h
index b8d23a52719..b72c3f067f1 100644
--- a/src/cbmc/symex_bmc.h
+++ b/src/cbmc/symex_bmc.h
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/message.h>
 
+#include <langapi/language_ui.h>
+
 #include <goto-symex/goto_symex.h>
 
 #include "symex_coverage.h"
@@ -28,6 +30,8 @@ class symex_bmct:
     symbol_tablet &_new_symbol_table,
     symex_targett &_target);
 
+  void set_ui(language_uit::uit _ui) { ui=_ui; }
+
   // To show progress
   source_locationt last_source_location;
 
@@ -64,6 +68,9 @@ class symex_bmct:
   bool record_coverage;
 
 protected:
+  // use gui format
+  language_uit::uit ui;
+
   // We have
   // 1) a global limit (max_unwind)
   // 2) a limit per loop, all threads
@@ -82,7 +89,7 @@ class symex_bmct:
   //
   // overloaded from goto_symext
   //
-  virtual void symex_step(
+  virtual bool symex_step(
     const goto_functionst &goto_functions,
     statet &state);
 
diff --git a/src/cbmc/symex_bmc_incremental.cpp b/src/cbmc/symex_bmc_incremental.cpp
new file mode 100644
index 00000000000..a5fd8bceb42
--- /dev/null
+++ b/src/cbmc/symex_bmc_incremental.cpp
@@ -0,0 +1,314 @@
+/*******************************************************************\
+
+Module: Incremental Bounded Model Checking for ANSI-C
+
+Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <limits>
+
+#include <util/source_location.h>
+
+#include "symex_bmc_incremental.h"
+
+/*******************************************************************\
+
+Function: symex_bmc_incrementalt::symex_bmct
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+symex_bmc_incrementalt::symex_bmc_incrementalt(
+  const namespacet &_ns,
+  symbol_tablet &_new_symbol_table,
+  symex_targett &_target):
+  symex_bmct(_ns, _new_symbol_table, _target)
+{
+  magic_numbers.insert(0);
+  magic_numbers.insert(1);
+  magic_numbers.insert(2);
+  magic_numbers.insert(6);
+  magic_numbers.insert(12);
+  magic_numbers.insert(17);
+  magic_numbers.insert(21);
+  magic_numbers.insert(40);
+  magic_numbers.insert(60);
+  magic_numbers.insert(80);
+  magic_numbers.insert(100);
+  magic_numbers.insert(200);
+  magic_numbers.insert(1025);
+}
+// magic numbers are heuristic unwinding numbers used for SV_COMP
+/*******************************************************************\
+
+Function: symex_bmc_incrementalt::get_unwind
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool symex_bmc_incrementalt::get_unwind(
+  const symex_targett::sourcet &source,
+  unsigned unwind)
+{
+  const irep_idt id=goto_programt::loop_id(source.pc);
+
+  // We use the most specific limit we have,
+  // and 'infinity' when we have none.
+
+  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
+
+  loop_limitst &this_thread_limits=
+    thread_loop_limits[source.thread_nr];
+
+  loop_limitst::const_iterator l_it=this_thread_limits.find(id);
+  if(l_it!=this_thread_limits.end())
+    this_loop_limit=l_it->second;
+  else
+  {
+    l_it=loop_limits.find(id);
+    if(l_it!=loop_limits.end())
+      this_loop_limit=l_it->second;
+    else if(max_unwind_is_set)
+      this_loop_limit=max_unwind;
+  }
+
+  // use the incremental limits if
+  // it is the specified incremental loop or
+  // there was no non-incremental limit
+  if(this_loop_limit==std::numeric_limits<unsigned>::max())
+  {
+    this_loop_limit=incr_max_unwind;
+    if(unwind+1>=incr_min_unwind)
+      ignore_assertions=false;
+  }
+
+  bool abort=unwind>=this_loop_limit;
+
+  statistics() << (abort?"Not unwinding":"Unwinding")
+               << " loop " << id << " iteration "
+               << unwind;
+
+  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
+    statistics() << " (" << this_loop_limit << " max)";
+
+  statistics() << " " << source.pc->source_location
+               << " thread " << source.thread_nr << eom;
+
+  return abort;
+}
+
+/*******************************************************************\
+
+Function: symex_bmc_incrementalt::get_unwind_recursion
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool symex_bmc_incrementalt::get_unwind_recursion(
+  const irep_idt &id,
+  const unsigned thread_nr,
+  unsigned unwind)
+{
+  // We use the most specific limit we have,
+  // and 'infinity' when we have none.
+
+  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
+
+  loop_limitst &this_thread_limits=
+    thread_loop_limits[thread_nr];
+
+  loop_limitst::const_iterator l_it=this_thread_limits.find(id);
+  if(l_it!=this_thread_limits.end())
+    this_loop_limit=l_it->second;
+  else
+  {
+    l_it=loop_limits.find(id);
+    if(l_it!=loop_limits.end())
+      this_loop_limit=l_it->second;
+    else if(max_unwind_is_set)
+      this_loop_limit=max_unwind;
+  }
+
+  // use the incremental limits if
+  // it is the specified incremental loop or
+  // there was no non-incremental limit
+  if(this_loop_limit==std::numeric_limits<unsigned>::max())
+  {
+    this_loop_limit=incr_max_unwind;
+    if(unwind+1>=incr_min_unwind)
+      ignore_assertions=false;
+  }
+
+  bool abort=unwind>this_loop_limit;
+
+  if(unwind>0 || abort)
+  {
+    const symbolt &symbol=ns.lookup(id);
+
+    statistics() << (abort?"Not unwinding":"Unwinding")
+                 << " recursion "
+                 << symbol.display_name()
+                 << " iteration " << unwind;
+
+    if(this_loop_limit!=std::numeric_limits<unsigned>::max())
+      statistics() << " (" << this_loop_limit << " max)";
+
+    statistics() << eom;
+  }
+
+  return abort;
+}
+
+/*******************************************************************\
+
+Function: symex_bmc_incrementalt::check_break
+
+ Inputs: source of the current symbolic execution state
+
+ Outputs: true if the back edge encountered during symbolic execution
+            corresponds to the a loop that is handled incrementally
+
+ Purpose: defines condition for interrupting symbolic execution
+            for incremental BMC
+
+\*******************************************************************/
+
+bool symex_bmc_incrementalt::check_break(
+  const irep_idt &id,
+  bool is_function,
+  statet &state,
+  const exprt &cond,
+  unsigned unwind)
+{
+  if(unwind<incr_min_unwind)
+    return false;
+
+#if 0
+  std::cout << "loop limit for " << id
+            << (loop_limits.find(id)!=loop_limits.end() ?
+               " exists" : " does not exist") << "\n";
+#endif
+
+  loop_limitst &this_thread_limits=
+    thread_loop_limits[state.source.thread_nr];
+  if(this_thread_limits.find(id)==this_thread_limits.end() &&
+     loop_limits.find(id)==loop_limits.end())
+  {
+#if 0
+    std::cout << "not statically unwound \n";
+    // not a statically unwound loop when --incremental
+#endif
+
+    if(loop_cond.checked_function)
+    {
+      loop_cond.checked_function=false;
+      return false;
+    }
+
+    // continue symexing until the next magic unwinding number is reached
+    if(options.get_bool_option("magic-numbers") &&
+         magic_numbers.find(unwind)==magic_numbers.end())
+    {
+      return false;
+    }
+
+    // memorize unwinding assertion for loop check
+    exprt simplified_cond=not_exprt(cond);
+    do_simplify(simplified_cond);
+    state.rename(simplified_cond, ns);
+    state.guard.guard_expr(simplified_cond);
+
+    loop_cond.id=id;
+    loop_cond.cond=simplified_cond;
+    loop_cond.guard=state.guard.as_expr();
+    loop_cond.loop_info=&(state.top().loop_iterations[id]);
+    loop_cond.source=state.source;
+    if(is_function)
+      loop_cond.checked_function=true;
+
+    return true;
+  }
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: symex_bmc_incrementalt::add_loop_check
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool symex_bmc_incrementalt::add_loop_check()
+{
+  status() << "Checking loop/recursive call " << loop_cond.id << eom;
+
+#if 0
+  debug() << "Loop/recursive call condition: "
+          << from_expr(ns, "", loop_cond.cond) << eom;
+#endif
+
+  if(loop_cond.cond.is_false())
+  {
+    debug() << "Loop/recursive call " << loop_cond.id
+            << " not fully unwound" << eom;
+    return false;
+  }
+
+  if(options.get_bool_option("earliest-loop-exit"))
+    target.assertion(
+      loop_cond.guard,
+      not_exprt(loop_cond.cond),
+      SYMEX_CONTINUATION_CHECK,
+      loop_cond.source);
+  else
+    target.assertion(
+      loop_cond.guard,
+      loop_cond.cond,
+      SYMEX_CONTINUATION_CHECK,
+      loop_cond.source);
+
+  return true;
+}
+
+/*******************************************************************\
+
+Function: symex_bmc_incrementalt::update_loop_info
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void symex_bmc_incrementalt::update_loop_info(bool fully_unwound)
+{
+  status() << "Loop/recursive call " << loop_cond.id
+           << (fully_unwound ? " fully unwound" : " not fully unwound") << eom;
+
+  loop_cond.loop_info->fully_unwound=fully_unwound;
+  loop_cond.id="";
+}
diff --git a/src/cbmc/symex_bmc_incremental.h b/src/cbmc/symex_bmc_incremental.h
new file mode 100644
index 00000000000..97700fd3309
--- /dev/null
+++ b/src/cbmc/symex_bmc_incremental.h
@@ -0,0 +1,67 @@
+/*******************************************************************\
+
+Module: Incremental Bounded Model Checking for ANSI-C
+
+Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_CBMC_SYMEX_BMC_INCREMENTAL_H
+#define CPROVER_CBMC_SYMEX_BMC_INCREMENTAL_H
+
+#include "symex_bmc.h"
+
+class symex_bmc_incrementalt:
+  public symex_bmct
+{
+ public:
+  symex_bmc_incrementalt(
+    const namespacet &_ns,
+    symbol_tablet &_new_symbol_table,
+    symex_targett &_target);
+
+  unsigned incr_max_unwind;
+  unsigned incr_min_unwind;
+
+  bool add_loop_check();
+  void update_loop_info(bool fully_unwound);
+
+protected:
+  // incremental unwinding
+
+  // returns true if the symbolic execution is to be interrupted for checking
+  virtual bool check_break(
+    const irep_idt &id,
+    bool is_function,
+    statet &state,
+    const exprt &cond,
+    unsigned unwind);
+
+  // stores info to check whether loop has been fully unwound
+  typedef struct
+  {
+    irep_idt id;
+    exprt guard;
+    exprt cond;
+    goto_symex_statet::framet::loop_infot *loop_info;
+    symex_targett::sourcet source;
+    bool checked_function;
+  } loop_condt;
+
+  loop_condt loop_cond;
+
+  // set of unwindings to check incrementally
+  std::set<unsigned> magic_numbers;
+
+  // for loop unwinding
+  virtual bool get_unwind(
+    const symex_targett::sourcet &source,
+    unsigned unwind);
+
+  virtual bool get_unwind_recursion(
+    const irep_idt &identifier,
+    const unsigned thread_nr,
+    unsigned unwind);
+};
+
+#endif
diff --git a/src/cbmc/symex_bmc_incremental_one_loop.cpp b/src/cbmc/symex_bmc_incremental_one_loop.cpp
new file mode 100644
index 00000000000..40081fe6742
--- /dev/null
+++ b/src/cbmc/symex_bmc_incremental_one_loop.cpp
@@ -0,0 +1,132 @@
+/*******************************************************************\
+
+Module: Incremental Bounded Model Checking for ANSI-C
+
+Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <limits>
+#include <iostream>
+
+#include <util/source_location.h>
+#include <util/xml.h>
+
+#include "symex_bmc_incremental_one_loop.h"
+
+/*******************************************************************\
+
+Function: symex_bmct::get_unwind
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool symex_bmc_incremental_one_loopt::get_unwind(
+  const symex_targett::sourcet &source,
+  unsigned unwind)
+{
+  const irep_idt id=goto_programt::loop_id(source.pc);
+
+  // We use the most specific limit we have,
+  // and 'infinity' when we have none.
+
+  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
+
+  loop_limitst &this_thread_limits=
+    thread_loop_limits[source.thread_nr];
+
+  loop_limitst::const_iterator l_it=this_thread_limits.find(id);
+  if(l_it!=this_thread_limits.end())
+    this_loop_limit=l_it->second;
+  else
+  {
+    l_it=loop_limits.find(id);
+    if(l_it!=loop_limits.end())
+      this_loop_limit=l_it->second;
+    else if(max_unwind_is_set)
+      this_loop_limit=max_unwind;
+  }
+
+  // use the incremental limits if
+  // it is the specified incremental loop or
+  // there was no non-incremental limit
+  if(id==incr_loop_id)
+  {
+    this_loop_limit=incr_max_unwind;
+    if(unwind+1>=incr_min_unwind)
+      ignore_assertions=false;
+  }
+
+  bool abort=unwind>=this_loop_limit;
+
+  // report where we are
+  if(ui==ui_message_handlert::uit::XML_UI)
+  {
+    xmlt xml("current-unwinding");
+    xml.data=std::to_string(unwind);
+    std::cout << xml << "\n";
+  }
+
+  statistics() << (abort?"Not unwinding":"Unwinding")
+               << " loop " << id << " iteration "
+               << unwind;
+
+  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
+    statistics() << " (" << this_loop_limit << " max)";
+
+  statistics() << " " << source.pc->source_location
+               << " thread " << source.thread_nr << eom;
+
+  return abort;
+}
+
+ /*******************************************************************\
+
+Function: symex_bmct::check_break
+
+ Inputs: source of the current symbolic execution state
+
+ Outputs: true if the back edge encountered during symbolic execution
+            corresponds to the given loop (incr_loop_id)
+
+ Purpose: defines condition for interrupting symbolic execution
+            for incremental BMC
+
+\*******************************************************************/
+
+bool symex_bmc_incremental_one_loopt::check_break(
+  const irep_idt &id,
+  bool is_function,
+  statet &state,
+  const exprt &cond,
+  unsigned unwind)
+{
+  if(unwind<incr_min_unwind)
+    return false;
+
+#if 0
+  bool loop_limit_exists=loop_limits.find(id)!=loop_limits.end();
+  std::cout << "loop limit for " << id
+            << (loop_limit_exists ? " exists" : " does not exist") << std::endl;
+#endif
+
+#if 0
+  loop_limitst &this_thread_limits=
+    thread_loop_limits[state.source.thread_nr];
+  if(incr_loop_id=="" &&
+     this_thread_limits.find(id)==this_thread_limits.end() &&
+     loop_limits.find(id)==loop_limits.end())
+  {
+    std::cout << "not statically unwound" << std::endl;
+    // not a statically unwound loop when incremental
+  }
+#endif
+
+  // loop specified by incrementalcheck
+  return (id==incr_loop_id);
+}
diff --git a/src/cbmc/symex_bmc_incremental_one_loop.h b/src/cbmc/symex_bmc_incremental_one_loop.h
new file mode 100644
index 00000000000..501b0f817fa
--- /dev/null
+++ b/src/cbmc/symex_bmc_incremental_one_loop.h
@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module: Incremental Bounded Model Checking for ANSI-C
+
+Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_CBMC_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
+#define CPROVER_CBMC_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
+
+#include <limits>
+
+#include <util/message.h>
+
+#include <solvers/prop/prop_conv.h>
+
+#include "symex_bmc.h"
+
+class symex_bmc_incremental_one_loopt:
+  public symex_bmct
+{
+public:
+  symex_bmc_incremental_one_loopt(
+    const namespacet &_ns,
+    symbol_tablet &_new_symbol_table,
+    symex_targett &_target,
+    prop_convt& _prop_conv):
+    symex_bmct(_ns, _new_symbol_table, _target),
+    ignore_assertions(false),
+    incr_loop_id(""),
+    incr_max_unwind(std::numeric_limits<unsigned>::max()),
+    incr_min_unwind(0),
+    prop_conv(_prop_conv)
+  {}
+
+  bool ignore_assertions;
+  irep_idt incr_loop_id;
+  unsigned incr_max_unwind;
+  unsigned incr_min_unwind;
+
+protected:
+  // incremental unwinding
+  prop_convt &prop_conv;
+
+  // returns true if the symbolic execution is to be interrupted for checking
+  virtual bool check_break(
+    const irep_idt &id,
+    bool is_function,
+    goto_symext::statet &state,
+    const exprt &cond,
+    unsigned unwind);
+
+  // for loop unwinding
+  virtual bool get_unwind(
+    const symex_targett::sourcet &source,
+    unsigned unwind);
+};
+
+#endif
diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp
index 131438d1af6..5cdcaa6fb62 100644
--- a/src/goto-instrument/remove_function.cpp
+++ b/src/goto-instrument/remove_function.cpp
@@ -63,6 +63,7 @@ void remove_function(
 /// goto_functions  Input functions to be modified
 /// names  List of functions to be removed
 /// message_handler  Error/status output
+
 void remove_functions(
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions,
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index a5bf81a722d..3de38da7b8e 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -233,7 +233,7 @@ void goto_convertt::do_scanf(
 
   if(f_id==CPROVER_PREFIX "scanf")
   {
-    if(arguments.empty())
+    if(arguments.size()<1)
     {
       error().source_location=function.find_source_location();
       error() << "scanf takes at least one argument" << eom;
@@ -1328,7 +1328,7 @@ void goto_convertt::do_function_call_symbol(
   }
   else if(identifier==CPROVER_PREFIX "fence")
   {
-    if(arguments.empty())
+    if(arguments.size()<1)
     {
       error().source_location=function.find_source_location();
       error() << "`" << identifier
@@ -1767,77 +1767,6 @@ void goto_convertt::do_function_call_symbol(
 
     // void __sync_lock_release (type *ptr, ...)
   }
-  else if(identifier=="__builtin_isgreater" ||
-          identifier=="__builtin_isgreater" ||
-          identifier=="__builtin_isgreaterequal" ||
-          identifier=="__builtin_isless" ||
-          identifier=="__builtin_islessequal" ||
-          identifier=="__builtin_islessgreater" ||
-          identifier=="__builtin_isunordered")
-  {
-    // these support two double or two float arguments; we call the
-    // appropriate internal version
-    if(arguments.size()!=2 ||
-       (arguments[0].type()!=double_type() &&
-        arguments[0].type()!=float_type()) ||
-       (arguments[1].type()!=double_type() &&
-        arguments[1].type()!=float_type()))
-    {
-      error().source_location=function.find_source_location();
-      error() << "`" << identifier
-              << "' expected to have two float/double arguments"
-              << eom;
-      throw 0;
-    }
-
-    exprt::operandst new_arguments=arguments;
-
-    bool use_double=arguments[0].type()==double_type();
-    if(arguments[0].type()!=arguments[1].type())
-    {
-      if(use_double)
-        new_arguments[1].make_typecast(arguments[0].type());
-      else
-      {
-        new_arguments[0].make_typecast(arguments[1].type());
-        use_double=true;
-      }
-    }
-
-    code_typet f_type=to_code_type(function.type());
-    f_type.remove_ellipsis();
-    const typet &a_t=new_arguments[0].type();
-    f_type.parameters()=
-      code_typet::parameterst(2, code_typet::parametert(a_t));
-
-    // replace __builtin_ by CPROVER_PREFIX
-    std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
-    // append d or f for double/float
-    name+=use_double?'d':'f';
-
-    symbol_exprt new_function=function;
-    new_function.set_identifier(name);
-    new_function.type()=f_type;
-
-    code_function_callt function_call;
-    function_call.lhs()=lhs;
-    function_call.function()=new_function;
-    function_call.arguments()=new_arguments;
-    function_call.add_source_location()=function.source_location();
-
-    if(!symbol_table.has_symbol(name))
-    {
-      code_typet();
-      symbolt new_symbol;
-      new_symbol.base_name=name;
-      new_symbol.name=name;
-      new_symbol.type=f_type;
-      new_symbol.location=function.source_location();
-      symbol_table.add(new_symbol);
-    }
-
-    copy(function_call, FUNCTION_CALL, dest);
-  }
   else
   {
     do_function_call_symbol(*symbol);
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 69f35bbdbea..0a0c7cb7d79 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -259,7 +259,6 @@ void goto_convert(
   {
     goto_convert_functions.error() << e << messaget::eom;
   }
-
   if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
     throw 0;
 }
diff --git a/src/goto-programs/safety_checker.h b/src/goto-programs/safety_checker.h
index bb1492d6f53..4a4e174d3c1 100644
--- a/src/goto-programs/safety_checker.h
+++ b/src/goto-programs/safety_checker.h
@@ -29,7 +29,8 @@ class safety_checkert:public messaget
     const namespacet &_ns,
     message_handlert &_message_handler);
 
-  enum class resultt { SAFE, UNSAFE, ERROR };
+
+  enum class resultt { SAFE, UNSAFE, ERROR , UNKNOWN };
 
   // check whether all assertions in goto_functions are safe
   // if UNSAFE, then a trace is returned
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 7b6a367f6b2..3a874d2213c 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -138,6 +138,9 @@ void build_goto_trace(
 
     const symex_target_equationt::SSA_stept &SSA_step=*it;
 
+    if(SSA_step.ignore)
+      continue;
+
     if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
       continue;
 
@@ -193,6 +196,9 @@ void build_goto_trace(
           symex_target_equationt::assignment_typet::GUARD))
       continue;
 
+    if(SSA_step.comment==SYMEX_CONTINUATION_CHECK)
+      continue;
+
     goto_tracet::stepst &steps=time_map[current_time];
     steps.push_back(goto_trace_stept());
     goto_trace_stept &goto_trace_step=steps.back();
@@ -297,7 +303,8 @@ void build_goto_trace(
       s_it1=goto_trace.steps.begin();
       s_it1!=goto_trace.steps.end();
       s_it1++)
-    if(s_it1->is_assert() && !s_it1->cond_value)
+    if(s_it1->is_assert() && !s_it1->cond_value &&
+       s_it1->comment!=SYMEX_CONTINUATION_CHECK)
     {
       goto_trace.trim_after(s_it1);
       break;
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index f45d722ebf7..83a94d366cf 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -52,7 +52,7 @@ class goto_symext
     remaining_vccs(0),
     constant_propagation(true),
     new_symbol_table(_new_symbol_table),
-    language_mode(),
+    ignore_assertions(false),
     ns(_ns),
     target(_target),
     atomic_section_counter(0),
@@ -78,13 +78,13 @@ class goto_symext
     const goto_programt &goto_program);
 
   /** start symex in a given state */
-  virtual void operator()(
+  virtual bool operator()(
     statet &state,
     const goto_functionst &goto_functions,
     const goto_programt &goto_program);
 
   /** execute just one step */
-  virtual void symex_step(
+  virtual bool symex_step(
     const goto_functionst &goto_functions,
     statet &state);
 
@@ -98,6 +98,7 @@ class goto_symext
 
   optionst options;
   symbol_tablet &new_symbol_table;
+  bool ignore_assertions;
 
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.
@@ -110,6 +111,13 @@ class goto_symext
 
   friend class symex_dereference_statet;
 
+  virtual bool check_break(
+    const irep_idt &id,
+    bool is_function,
+    statet &state,
+    const exprt &cond,
+    unsigned unwind);
+
   void new_name(symbolt &symbol);
 
   // this does the following:
@@ -156,7 +164,7 @@ class goto_symext
 
   // symex
 
-  virtual void symex_goto(statet &state);
+  virtual bool symex_goto(statet &state);
   virtual void symex_start_thread(statet &state);
   virtual void symex_atomic_begin(statet &state);
   virtual void symex_atomic_end(statet &state);
@@ -207,19 +215,19 @@ class goto_symext
   {
   }
 
-  virtual void symex_function_call(
+  virtual bool symex_function_call(
     const goto_functionst &goto_functions,
     statet &state,
     const code_function_callt &call);
 
   virtual void symex_end_of_function(statet &state);
 
-  virtual void symex_function_call_symbol(
+  virtual bool symex_function_call_symbol(
     const goto_functionst &goto_functions,
     statet &state,
     const code_function_callt &call);
 
-  virtual void symex_function_call_code(
+  virtual bool symex_function_call_code(
     const goto_functionst &goto_functions,
     statet &state,
     const code_function_callt &call);
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index d62d4a66af9..a196cb4c25e 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -26,6 +26,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class dirtyt;
 
+#define SYMEX_CONTINUATION_CHECK "symex_continuation_check"
+
+
 // central data structure: state
 class goto_symex_statet
 {
@@ -265,11 +268,13 @@ class goto_symex_statet
     {
       loop_infot():
         count(0),
+        fully_unwound(false),
         is_recursion(false)
       {
       }
 
       unsigned count;
+      bool fully_unwound;
       bool is_recursion;
     };
     typedef std::unordered_map<irep_idt, loop_infot, irep_id_hash>
diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp
index a398264963e..4343da2dfb2 100644
--- a/src/goto-symex/slice.cpp
+++ b/src/goto-symex/slice.cpp
@@ -261,3 +261,22 @@ void simple_slice(symex_target_equationt &equation)
       s_it->ignore=true;
   }
 }
+
+/*******************************************************************\
+
+Function: undo_slice
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void undo_slice(symex_target_equationt &equation)
+{
+  // set ignore to false
+  for(auto & it : equation.SSA_steps)
+    it.ignore=false;
+}
diff --git a/src/goto-symex/slice.h b/src/goto-symex/slice.h
index 2bc887a0c9f..d8077c3a5b9 100644
--- a/src/goto-symex/slice.h
+++ b/src/goto-symex/slice.h
@@ -24,6 +24,9 @@ void simple_slice(symex_target_equationt &equation);
 void slice(symex_target_equationt &equation,
            const expr_listt &expressions);
 
+// Undo symex slicing
+void undo_slice(symex_target_equationt &equation);
+
 // Collects "open" variables that are used but not assigned
 
 typedef std::unordered_set<irep_idt, irep_id_hash> symbol_sett;
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index e50d1c8ea7f..20190a4aadd 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -169,7 +169,8 @@ void goto_symext::parameter_assignments(
   }
 }
 
-void goto_symext::symex_function_call(
+
+bool goto_symext::symex_function_call(
   const goto_functionst &goto_functions,
   statet &state,
   const code_function_callt &code)
@@ -177,7 +178,7 @@ void goto_symext::symex_function_call(
   const exprt &function=code.function();
 
   if(function.id()==ID_symbol)
-    symex_function_call_symbol(goto_functions, state, code);
+    return symex_function_call_symbol(goto_functions, state, code);
   else if(function.id()==ID_if)
     throw "symex_function_call can't do if";
   else if(function.id()==ID_dereference)
@@ -186,7 +187,8 @@ void goto_symext::symex_function_call(
     throw "unexpected function for symex_function_call: "+function.id_string();
 }
 
-void goto_symext::symex_function_call_symbol(
+
+bool goto_symext::symex_function_call_symbol(
   const goto_functionst &goto_functions,
   statet &state,
   const code_function_callt &code)
@@ -211,11 +213,13 @@ void goto_symext::symex_function_call_symbol(
     symex_macro(state, code);
   }
   else
-    symex_function_call_code(goto_functions, state, code);
+    return symex_function_call_code(goto_functions, state, code);
+
+  return false;
 }
 
 /// do function call by inlining
-void goto_symext::symex_function_call_code(
+bool goto_symext::symex_function_call_code(
   const goto_functionst &goto_functions,
   statet &state,
   const code_function_callt &call)
@@ -255,7 +259,7 @@ void goto_symext::symex_function_call_code(
     }
 
     state.source.pc++;
-    return;
+    return false;
   }
 
   // record the call
@@ -277,7 +281,7 @@ void goto_symext::symex_function_call_code(
     }
 
     state.source.pc++;
-    return;
+    return false;
   }
 
   // read the arguments -- before the locality renaming
@@ -315,6 +319,8 @@ void goto_symext::symex_function_call_code(
 
   state.source.is_set=true;
   state.source.pc=goto_function.body.instructions.begin();
+
+  return false;
 }
 
 /// pop one call frame
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 03186a129b3..d535d7e4329 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -12,13 +12,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 #include <algorithm>
 
+#include <util/expr_util.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
 #include <analyses/dirty.h>
 
 #include "goto_symex.h"
 
-void goto_symext::symex_goto(statet &state)
+
+bool goto_symext::symex_goto(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
   statet::framet &frame=state.top();
@@ -30,7 +33,12 @@ void goto_symext::symex_goto(statet &state)
   state.rename(new_guard, ns);
   do_simplify(new_guard);
 
-  if(new_guard.is_false() ||
+  const irep_idt loop_id=goto_programt::loop_id(state.source.pc);
+
+  // Testing for "is_false":
+  // we need to explicitly simplify despite "no-simplify".
+  const exprt incr_test_guard=simplify_expr(old_guard, ns);
+  if(incr_test_guard.is_false() || new_guard.is_false() ||
      state.guard.is_false())
   {
     if(!state.guard.is_false())
@@ -38,11 +46,16 @@ void goto_symext::symex_goto(statet &state)
 
     // reset unwinding counter
     if(instruction.is_backwards_goto())
-      frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count=0;
+    {
+      goto_symex_statet::framet::loop_infot &loop_info=
+        frame.loop_iterations[loop_id];
+      loop_info.count=0;
+      loop_info.fully_unwound=false;
+    }
 
     // next instruction
     state.source.pc++;
-    return; // nothing to do
+    return false; // nothing to do
   }
 
   target.goto_instruction(state.guard.as_expr(), new_guard, state.source);
@@ -78,15 +91,17 @@ void goto_symext::symex_goto(statet &state)
 
       // next instruction
       state.source.pc++;
-      return;
+      return false;
     }
 
-    unsigned &unwind=
-      frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count;
+    goto_symex_statet::framet::loop_infot &loop_info=
+      frame.loop_iterations[loop_id];
+    unsigned &unwind=loop_info.count;
+
     unwind++;
 
     // continue unwinding?
-    if(get_unwind(state.source, unwind))
+    if(loop_info.fully_unwound || get_unwind(state.source, unwind))
     {
       // no!
       loop_bound_exceeded(state, new_guard);
@@ -96,13 +111,16 @@ void goto_symext::symex_goto(statet &state)
 
       // next instruction
       state.source.pc++;
-      return;
+
+      // do not break, but continue symex to the end of the program
+      return false;
     }
 
-    if(new_guard.is_true())
+    if(new_guard.is_true()) // continue looping
     {
+      bool do_break=check_break(loop_id, false, state, new_guard, unwind);
       state.source.pc=goto_target;
-      return; // nothing else to do
+      return do_break;
     }
   }
 
@@ -123,7 +141,7 @@ void goto_symext::symex_goto(statet &state)
     if(state_pc==goto_target)
     {
       state.source.pc=goto_target;
-      return; // nothing else to do
+      return false; // nothing else to do
     }
   }
   else
@@ -195,8 +213,22 @@ void goto_symext::symex_goto(statet &state)
       new_state.guard.add(guard_expr);
     }
   }
+  return false;
 }
 
+
+bool goto_symext::check_break(
+  const irep_idt &id,
+  bool is_function,
+  statet &state,
+  const exprt &cond,
+  unsigned unwind)
+{
+  // dummy implementation
+  return false;
+}
+
+
 void goto_symext::symex_step_goto(statet &state, bool taken)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
@@ -377,6 +409,7 @@ void goto_symext::phi_function(
   }
 }
 
+
 void goto_symext::loop_bound_exceeded(
   statet &state,
   const exprt &guard)
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 501fdabea70..7de42bf8e03 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -98,14 +98,17 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
   }
 }
 
+
 /// symex from given state
-void goto_symext::operator()(
+bool goto_symext::operator()(
   statet &state,
   const goto_functionst &goto_functions,
   const goto_programt &goto_program)
 {
   assert(!goto_program.instructions.empty());
 
+  if(state.symex_target==NULL)
+  {
   state.source=symex_targett::sourcet(goto_program);
   assert(!state.threads.empty());
   assert(!state.call_stack().empty());
@@ -113,12 +116,14 @@ void goto_symext::operator()(
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=&target;
   state.dirty=new dirtyt(goto_functions);
+  }
 
   assert(state.top().end_of_function->is_end_function());
 
   while(!state.call_stack().empty())
   {
-    symex_step(goto_functions, state);
+    if(symex_step(goto_functions, state))
+      return false;
 
     // is there another thread to execute?
     if(state.call_stack().empty() &&
@@ -132,6 +137,7 @@ void goto_symext::operator()(
 
   delete state.dirty;
   state.dirty=0;
+  return true;
 }
 
 /// symex starting from given program
@@ -157,8 +163,9 @@ void goto_symext::operator()(const goto_functionst &goto_functions)
   operator()(goto_functions, body);
 }
 
+
 /// do just one step
-void goto_symext::symex_step(
+bool goto_symext::symex_step(
   const goto_functionst &goto_functions,
   statet &state)
 {
@@ -207,7 +214,7 @@ void goto_symext::symex_step(
     break;
 
   case GOTO:
-    symex_goto(state);
+    return symex_goto(state);
     break;
 
   case ASSUME:
@@ -223,7 +230,7 @@ void goto_symext::symex_step(
     break;
 
   case ASSERT:
-    if(!state.guard.is_false())
+    if(!state.guard.is_false() && !ignore_assertions)
     {
       std::string msg=id2string(state.source.pc->source_location.get_comment());
       if(msg=="")
@@ -264,7 +271,33 @@ void goto_symext::symex_step(
       Forall_expr(it, deref_code.arguments())
         clean_expr(*it, state, false);
 
-      symex_function_call(goto_functions, state, deref_code);
+      const irep_idt &identifier=
+        to_symbol_expr(deref_code.function()).get_identifier();
+      const goto_symex_statet::framet::loop_infot &loop_info =
+        state.top().loop_iterations[identifier];
+
+      if(!loop_info.fully_unwound)
+      {
+        goto_functionst::function_mapt::const_iterator it=
+          goto_functions.function_map.find(identifier);
+        assert(goto_functions.function_map.find(identifier)!=
+               goto_functions.function_map.end());
+
+        // interrupt for checking guard if in incremental mode
+        if(!state.guard.is_true() &&
+           // no need to check recursive call if function body is not available
+           it->second.body_available())
+        {
+          exprt guard=state.guard.as_expr();
+          bool do_break=
+            check_break(identifier, true, state, guard, loop_info.count);
+          if(do_break)
+            return true;
+        }
+        return symex_function_call(goto_functions, state, deref_code);
+      }
+      else
+        state.source.pc++;
     }
     else
       state.source.pc++;
@@ -327,4 +360,5 @@ void goto_symext::symex_step(
   default:
     throw "symex got unexpected instruction";
   }
+  return false;
 }
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index e0c8e86a42f..27a39892bbd 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -12,6 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include <util/std_expr.h>
+#include <solvers/prop/literal_expr.h>
+#include <util/expr_util.h>
+
 
 #include <langapi/language_util.h>
 #include <solvers/prop/prop_conv.h>
@@ -22,7 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "symex_target_equation.h"
 
 symex_target_equationt::symex_target_equationt(
-  const namespacet &_ns):ns(_ns)
+  const namespacet &_ns):is_incremental(false), ns(_ns), io_count(0)
 {
 }
 
@@ -392,24 +395,28 @@ void symex_target_equationt::convert(
 /// \par parameters: decision procedure
 /// \return -
 void symex_target_equationt::convert_assignments(
-  decision_proceduret &decision_procedure) const
+  decision_proceduret &decision_procedure)
 {
-  for(const auto &step : SSA_steps)
+  for(auto &step : SSA_steps)
   {
-    if(step.is_assignment() && !step.ignore)
+    if(step.is_assignment() && !step.ignore && !step.converted)
+  {
+      step.converted=true;
       decision_procedure.set_to_true(step.cond_expr);
   }
+  }
 }
 
 /// converts declarations
 /// \return -
 void symex_target_equationt::convert_decls(
-  prop_convt &prop_conv) const
+  prop_convt &prop_conv)
 {
-  for(const auto &step : SSA_steps)
+  for(auto &step : SSA_steps)
   {
-    if(step.is_decl() && !step.ignore)
+    if(step.is_decl() && !step.ignore && !step.converted)
     {
+      step.converted=true;
       // The result is not used, these have no impact on
       // the satisfiability of the formula.
       prop_conv.convert(step.cond_expr);
@@ -469,15 +476,16 @@ void symex_target_equationt::convert_goto_instructions(
 /// \par parameters: decision procedure
 /// \return -
 void symex_target_equationt::convert_constraints(
-  decision_proceduret &decision_procedure) const
+  decision_proceduret &decision_procedure)
 {
-  for(const auto &step : SSA_steps)
+  for(auto &step : SSA_steps)
   {
     if(step.is_constraint())
     {
-      if(step.ignore)
+      if(step.ignore || step.converted)
         continue;
 
+      step.converted=true;
       decision_procedure.set_to_true(step.cond_expr);
     }
   }
@@ -496,19 +504,68 @@ void symex_target_equationt::convert_assertions(
   if(number_of_assertions==0)
     return;
 
+  exprt assumption=true_exprt();
+
+  // literal a_k to be added to assertions clauses
+  // to de-/activate them for incr. solving
+  literalt activation_literal;
+  if(is_incremental)
+  {
+    activation_literal=prop_conv.convert(
+      symbol_exprt("symex::act$"+
+                   std::to_string(activate_assertions.size()), bool_typet()));
+
+    if(!activate_assertions.empty())
+    {
+      literalt last_activation_literal=activate_assertions.back();
+      activate_assertions.pop_back();
+      activate_assertions.push_back(!last_activation_literal);
+    }
+    activate_assertions.push_back(!activation_literal);
+
+    // set assumptions (a_0 ... -a_k) for incremental solving
+    prop_conv.set_assumptions(activate_assertions);
+  }
+
   if(number_of_assertions==1)
   {
     for(auto &step : SSA_steps)
     {
-      if(step.is_assert())
+      // ignore already converted assertions in the error trace
+      if(step.is_assert() && step.converted)
+        step.ignore=true;
+
+      if(step.is_assert() && !step.ignore && !step.converted)
+      {
+        step.converted=true;
+
+        if(is_incremental)
       {
+          prop_conv.set_to_true(
+            or_exprt(
+              literal_exprt(activation_literal),
+              not_exprt(step.cond_expr)));
+        }
+        else
         prop_conv.set_to_false(step.cond_expr);
+
         step.cond_literal=const_literal(false);
+
         return; // prevent further assumptions!
       }
       else if(step.is_assume())
+      {
+        if(is_incremental)
+        {
+          prop_conv.set_to_true(
+            or_exprt(
+              literal_exprt(activation_literal),
+              step.cond_expr));
+        }
+        else
         prop_conv.set_to_true(step.cond_expr);
     }
+    }
 
     assert(false); // unreachable
   }
@@ -516,21 +573,30 @@ void symex_target_equationt::convert_assertions(
   // We do (NOT a1) OR (NOT a2) ...
   // where the a's are the assertions
   or_exprt::operandst disjuncts;
-  disjuncts.reserve(number_of_assertions);
+  disjuncts.reserve(
+    is_incremental ? number_of_assertions+1 : number_of_assertions);
 
-  exprt assumption=true_exprt();
+  if(is_incremental)
+  {
+    // assumptions for incremental solving:
+    // (a_0 ... -a_k-1) --> (a_0 ... a_k-1 -a_k)
+    disjuncts.push_back(literal_exprt(activation_literal));
+  }
 
   for(auto &step : SSA_steps)
   {
-    if(step.is_assert())
+    // ignore already converted assertions in the error trace
+    if(step.is_assert() && step.converted)
+      step.ignore=true;
+
+    if(step.is_assert() && !step.ignore && !step.converted)
     {
-      implies_exprt implication(
-        assumption,
-        step.cond_expr);
+      step.converted=true;
+
+      implies_exprt implication(assumption, step.cond_expr);
 
       // do the conversion
       step.cond_literal=prop_conv.convert(implication);
-
       // store disjunct
       disjuncts.push_back(literal_exprt(!step.cond_literal));
     }
@@ -550,16 +616,47 @@ void symex_target_equationt::convert_assertions(
   prop_conv.set_to_true(disjunction(disjuncts));
 }
 
+
 /// converts I/O
 /// \par parameters: decision procedure
 /// \return -
+
+literalt symex_target_equationt::current_activation_literal()
+{
+  if(!is_incremental)
+    return const_literal(false);
+
+  return !activate_assertions.back();
+}
+
+void symex_target_equationt::new_activation_literal(prop_convt &prop_conv)
+{
+  if(is_incremental)
+  {
+    literalt activation_literal=prop_conv.convert(
+      symbol_exprt("symex::act$"+
+                   std::to_string(activate_assertions.size()), bool_typet()));
+
+    if(!activate_assertions.empty())
+    {
+      literalt last_activation_literal=activate_assertions.back();
+      activate_assertions.pop_back();
+      activate_assertions.push_back(!last_activation_literal);
+    }
+    activate_assertions.push_back(!activation_literal);
+
+    // set assumptions (a_0 ... -a_k) for incremental solving
+    prop_conv.set_assumptions(activate_assertions);
+  }
+}
+
 void symex_target_equationt::convert_io(
   decision_proceduret &dec_proc)
 {
   unsigned io_count=0;
 
   for(auto &step : SSA_steps)
-    if(!step.ignore)
+    if(!step.ignore && !step.converted)
     {
       for(const auto &arg : step.io_args)
       {
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index abee81346a7..cd52ecca40f 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -156,14 +156,14 @@ class symex_target_equationt:public symex_targett
     const sourcet &source);
 
   void convert(prop_convt &prop_conv);
-  void convert_assignments(decision_proceduret &decision_procedure) const;
-  void convert_decls(prop_convt &prop_conv) const;
+  void convert_assignments(decision_proceduret &decision_procedure);
+  void convert_decls(prop_convt &prop_conv);
   void convert_assumptions(prop_convt &prop_conv);
   void convert_assertions(prop_convt &prop_conv);
-  void convert_constraints(decision_proceduret &decision_procedure) const;
-  void convert_goto_instructions(prop_convt &prop_conv);
+  void convert_constraints(decision_proceduret &decision_procedure);
   void convert_guards(prop_convt &prop_conv);
   void convert_io(decision_proceduret &decision_procedure);
+  void convert_goto_instructions(prop_convt &prop_conv);
 
   exprt make_expression() const;
 
@@ -238,6 +238,9 @@ class symex_target_equationt:public symex_targett
     // for slicing
     bool ignore;
 
+    // for incremental conversion
+    bool converted;
+
     SSA_stept():
       type(goto_trace_stept::typet::NONE),
       hidden(false),
@@ -251,7 +254,8 @@ class symex_target_equationt:public symex_targett
       cond_literal(const_literal(false)),
       formatted(false),
       atomic_section_id(0),
-      ignore(false)
+      ignore(false),
+      converted(false)
     {
     }
 
@@ -282,6 +286,12 @@ class symex_target_equationt:public symex_targett
     return i;
   }
 
+  // for incremental solving
+  bool is_incremental;
+  bvt activate_assertions;
+  literalt current_activation_literal();
+  void new_activation_literal(prop_convt &prop_conv);
+
   typedef std::list<SSA_stept> SSA_stepst;
   SSA_stepst SSA_steps;
 
@@ -316,6 +326,7 @@ class symex_target_equationt:public symex_targett
 
 protected:
   const namespacet &ns;
+  unsigned io_count;
 
   // for enforcing sharing in the expressions stored
   merge_irept merge_irep;
diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp
index 1783983ccf9..7695f789bb3 100644
--- a/src/solvers/prop/cover_goals.cpp
+++ b/src/solvers/prop/cover_goals.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "literal_expr.h"
 #include "cover_goals.h"
 
+
 cover_goalst::~cover_goalst()
 {
 }
@@ -38,12 +39,15 @@ void cover_goalst::mark()
     }
 }
 
+
 /// Build clause
+
 void cover_goalst::constraint()
 {
   exprt::operandst disjuncts;
 
   // cover at least one unknown goal
+  disjuncts.push_back(literal_exprt(activation_literal));
 
   for(std::list<goalt>::const_iterator
       g_it=goals.begin();
diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h
index 8851e188347..ae6301740aa 100644
--- a/src/solvers/prop/cover_goals.h
+++ b/src/solvers/prop/cover_goals.h
@@ -22,6 +22,7 @@ class cover_goalst:public messaget
 {
 public:
   explicit cover_goalst(prop_convt &_prop_conv):
+    activation_literal(const_literal(false)),
     prop_conv(_prop_conv)
   {
   }
@@ -45,6 +46,7 @@ class cover_goalst:public messaget
 
   typedef std::list<goalt> goalst;
   goalst goals;
+  literalt activation_literal; // for incremental solving
 
   // statistics
 
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index cc022538949..63730d1cf9a 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Expression Representation
 
+#include <cassert>
 #include <stack>
 
 #include "string2int.h"