diff --git a/.travis.yml b/.travis.yml
index 3a89ddf1e71..db76e3f04ff 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -303,6 +303,7 @@ install:
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
+  - UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-paths-lifo
   - scripts/delete_failing_smt2_solver_tests ; env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
   - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test
diff --git a/buildspec-windows.yml b/buildspec-windows.yml
index 8a7c248abc6..dc8c4561c61 100644
--- a/buildspec-windows.yml
+++ b/buildspec-windows.yml
@@ -40,6 +40,10 @@ phases:
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" '
 
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-paths-lifo BUILD_ENV=MSVC" '
+
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" '
diff --git a/buildspec.yml b/buildspec.yml
index e11d3fe33ca..e8a7a453e25 100644
--- a/buildspec.yml
+++ b/buildspec.yml
@@ -25,6 +25,7 @@ phases:
     commands:
       - make -C unit test
       - make -C regression test
+      - make -C regression/cbmc test-paths-lifo
       - scripts/delete_failing_smt2_solver_tests
       - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
index bb900107e38..954598f0b0f 100644
--- a/regression/cbmc/CMakeLists.txt
+++ b/regression/cbmc/CMakeLists.txt
@@ -1,3 +1,10 @@
 add_test_pl_tests(
     "$<TARGET_FILE:cbmc> --validate-goto-model" -X smt-backend
 )
+
+add_test_pl_profile(
+    "cbmc-paths-lifo"
+    "$<TARGET_FILE:cbmc> --paths lifo"
+    "-C;-X;thorough-paths;-X;smt-backend;-s;paths-lifo"
+    "CORE"
+)
diff --git a/regression/cbmc/Failing_Assert1/test.desc b/regression/cbmc/Failing_Assert1/test.desc
index eb20420afda..3acca2686a9 100644
--- a/regression/cbmc/Failing_Assert1/test.desc
+++ b/regression/cbmc/Failing_Assert1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^Runtime decision procedure: [0-9]+(\.[0-9]+)?s$
+^Runtime decision procedure: [0-9]+(\.[0-9]+(e-[0-9]+)?)?s$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
index 41cc877803e..8242ae26e44 100644
--- a/regression/cbmc/Makefile
+++ b/regression/cbmc/Makefile
@@ -6,6 +6,9 @@ test:
 test-cprover-smt2:
 	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
 
+test-paths-lifo:
+	@../test.pl -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend
+
 tests.log: ../test.pl test
 
 show:
diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc
index 6a638d1e767..6694cf6e8b7 100644
--- a/regression/cbmc/Multi_Dimensional_Array6/test.desc
+++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
 main.c
 --unwind 3 --no-unwinding-assertions
 ^EXIT=10$
diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
index 161958f9d5d..d68272d8db5 100644
--- a/regression/cbmc/address_space_size_limit1/test.desc
+++ b/regression/cbmc/address_space_size_limit1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects
diff --git a/regression/cbmc/array-tests/test.desc b/regression/cbmc/array-tests/test.desc
index 9efefbc7362..969d6de00f8 100644
--- a/regression/cbmc/array-tests/test.desc
+++ b/regression/cbmc/array-tests/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE thorough-paths
 main.c
 
 ^EXIT=0$