diff --git a/COMPILING.md b/COMPILING.md
index 44760d2b26a..86ff874d556 100644
--- a/COMPILING.md
+++ b/COMPILING.md
@@ -46,6 +46,19 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    make
    ```
 
+4. Linking against an IPASIR SAT solver
+
+   Get an IPASIR package and build picosat by default
+   ```
+   make -C src ipasir-build
+   ```
+
+   Build CBMC with IPASIR and link against the ipasir solver library
+   Note: the LIBSOLVER variable could be pointed towards other solvers
+   ```
+   make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a
+   ```
+
 # COMPILATION ON SOLARIS 11
 
 1. As root, get the necessary development tools:
diff --git a/regression/cbmc-concurrency/pthread_join1/test.desc b/regression/cbmc-concurrency/pthread_join1/test.desc
index 41b36c525bf..bf4baf2d440 100644
--- a/regression/cbmc-concurrency/pthread_join1/test.desc
+++ b/regression/cbmc-concurrency/pthread_join1/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] assertion i==1: FAILURE$
 ^\[main\.assertion\.2\] assertion i==2: SUCCESS$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc
index d1779e15ce6..6fe0cd3a5f0 100644
--- a/regression/cbmc-cover/mcdc1/test.desc
+++ b/regression/cbmc-cover/mcdc1/test.desc
@@ -10,6 +10,5 @@ main.c
 ^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
 ^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 10 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc11/test.desc b/regression/cbmc-cover/mcdc11/test.desc
index 2358a5feb12..2027e1577be 100644
--- a/regression/cbmc-cover/mcdc11/test.desc
+++ b/regression/cbmc-cover/mcdc11/test.desc
@@ -10,6 +10,5 @@ main.c
 ^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && D != FALSE.*: SATISFIED$
 ^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!\(C != FALSE\) && !\(D != FALSE\).*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 6 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc12/test.desc b/regression/cbmc-cover/mcdc12/test.desc
index 341ceb9da53..03a731e6d27 100644
--- a/regression/cbmc-cover/mcdc12/test.desc
+++ b/regression/cbmc-cover/mcdc12/test.desc
@@ -13,6 +13,5 @@ main.c
 ^\[main.coverage.20\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && F != FALSE.*: SATISFIED$
 ^\[main.coverage.21\] file main.c line 25 function main MC/DC independence condition `!\(E != FALSE\) && !\(F != FALSE\).*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 10 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc14/test.desc b/regression/cbmc-cover/mcdc14/test.desc
index de3fd57033c..09cf68d35d2 100644
--- a/regression/cbmc-cover/mcdc14/test.desc
+++ b/regression/cbmc-cover/mcdc14/test.desc
@@ -6,6 +6,5 @@ main.c
 ^\[main.coverage.1\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
 ^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 2 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc
index 0a531a3b9ba..396c7cd5e0d 100644
--- a/regression/cbmc-cover/mcdc3/test.desc
+++ b/regression/cbmc-cover/mcdc3/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && !\(x > \(unsigned int\)3\).*: SATISFIED$
 ^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < \(unsigned int\)5 && x > \(unsigned int\)3.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 4 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc
index 9ed8f0e7fce..1c469418a26 100644
--- a/regression/cbmc-cover/mcdc4/test.desc
+++ b/regression/cbmc-cover/mcdc4/test.desc
@@ -9,6 +9,5 @@ main.c
 ^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
 ^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 9 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc
index 7f5289c868d..267488742c2 100644
--- a/regression/cbmc-cover/mcdc6/test.desc
+++ b/regression/cbmc-cover/mcdc6/test.desc
@@ -6,6 +6,5 @@ main.c
 ^\[main.coverage.1\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* false: SATISFIED$
 ^\[main.coverage.2\] file main.c line 7 function main decision/condition `x < \(unsigned int\)3.* true: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 2 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc
index 7df603190cd..c288cbab0ce 100644
--- a/regression/cbmc-cover/mcdc7/test.desc
+++ b/regression/cbmc-cover/mcdc7/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.coverage.3\] file main.c line 8 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
 ^\[main.coverage.4\] file main.c line 8 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 2 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc
index f1711f5c8d1..43a1b2ca741 100644
--- a/regression/cbmc-cover/mcdc8/test.desc
+++ b/regression/cbmc-cover/mcdc8/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !\(a != FALSE\) && !\(b != FALSE\).* SATISFIED$
 ^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!\(c != FALSE\) && a != FALSE && !\(b != FALSE\).* SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 6 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-cover/mcdc9/test.desc b/regression/cbmc-cover/mcdc9/test.desc
index 3dbd096e9be..199f3f14885 100644
--- a/regression/cbmc-cover/mcdc9/test.desc
+++ b/regression/cbmc-cover/mcdc9/test.desc
@@ -9,6 +9,5 @@ main.c
 ^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && B != FALSE && C != FALSE && !\(D != FALSE\).* SATISFIED$
 ^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!\(A != FALSE\) && !\(B != FALSE\) && C != FALSE && !\(D != FALSE\).* SATISFIED$
 ^\*\* .* of .* covered \(100.0%\)$
-^\*\* Used 8 iterations$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/exceptions1/test.desc b/regression/cbmc-java/exceptions1/test.desc
index 1405444f649..bf588a879d5 100644
--- a/regression/cbmc-java/exceptions1/test.desc
+++ b/regression/cbmc-java/exceptions1/test.desc
@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file test.java line 26 function.*: FAILURE$
-\*\* 1 of [0-9]* failed \(2 iterations\)$
+\*\* 1 of [0-9]* failed 
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc-java/exceptions2/test.desc b/regression/cbmc-java/exceptions2/test.desc
index 724e37b0677..85422de8707 100644
--- a/regression/cbmc-java/exceptions2/test.desc
+++ b/regression/cbmc-java/exceptions2/test.desc
@@ -4,7 +4,7 @@ test.class
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file test.java line 15 function.*: FAILURE$
-^\*\* 1 of [0-9]* failed \(2 iterations\)$
+^\*\* 1 of [0-9]* failed 
 ^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..c171dd49a18 100644
--- a/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
+++ b/regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc
@@ -5,6 +5,6 @@ main.c
 ^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$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
index cf4a284351e..ad9c2b40bd5 100644
--- a/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
+++ b/regression/cbmc-with-incr/Pointer_byte_extract2/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] .*: FAILED$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^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..47c1a75edbe 100644
--- a/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
+++ b/regression/cbmc-with-incr/Pointer_byte_extract5/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+^\*\* 1 of 9 failed 
 --
 ^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..a8688dd7116 100644
--- a/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
+++ b/regression/cbmc-with-incr/Pointer_byte_extract8/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+^\*\* 1 of 9 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc-with-incr/pipe1/test.desc b/regression/cbmc-with-incr/pipe1/test.desc
index 95e607f531d..0d1e9fa0dba 100644
--- a/regression/cbmc-with-incr/pipe1/test.desc
+++ b/regression/cbmc-with-incr/pipe1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.4\] assertion data\[1\]==31: FAILED$
-^\*\* 1 of 5 failed \(2 iterations\)$
+^\*\* 1 of 5 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc
index 4bd6cbdc141..4827431dc9c 100644
--- a/regression/cbmc/Malloc23/test.desc
+++ b/regression/cbmc/Malloc23/test.desc
@@ -7,6 +7,6 @@ pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
 pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
-\*\* 4 of 36 failed \(3 iterations\)
+\*\* 4 of 36 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc
index 101a4c0e3bf..a0a32880488 100644
--- a/regression/cbmc/Multi_Dimensional_Array6/test.desc
+++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main\.assertion\.1\] : SUCCESS$
 ^\[main\.assertion\.2\] : FAILURE$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc
index 888430312a7..eb98d4f78ba 100644
--- a/regression/cbmc/Pointer_byte_extract2/test.desc
+++ b/regression/cbmc/Pointer_byte_extract2/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] .*: FAILURE$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc
index 8c70c85ee47..fa59dbff9dc 100644
--- a/regression/cbmc/Pointer_byte_extract5/test.desc
+++ b/regression/cbmc/Pointer_byte_extract5/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE
-\*\* 1 of 11 failed \(2 iterations\)
+\*\* 1 of 11 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc
index 801d41ee41b..25368d1f99d 100644
--- a/regression/cbmc/Pointer_byte_extract8/test.desc
+++ b/regression/cbmc/Pointer_byte_extract8/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+^\*\* 1 of 9 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
index df26ad98dbe..ccab2f3936c 100644
--- a/regression/cbmc/Quantifiers-assertion/test.desc
+++ b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -8,5 +8,5 @@ main.c
 ^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
 ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
-^\*\* 2 of 6 failed \(2 iterations\)$
+^\*\* 2 of 6 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
index ca5f55d51a2..f9886ec28be 100644
--- a/regression/cbmc/Quantifiers-assignment/test.desc
+++ b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -6,5 +6,5 @@ main.c
 ^\[main.assertion.2\] assertion y: FAILURE$
 ^\[main.assertion.3\] assertion z1: SUCCESS$
 ^\[main.assertion.4\] assertion z2: SUCCESS$
-^\*\* 1 of 4 failed \(2 iterations\)$
+^\*\* 1 of 4 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc
index 7685cf4284a..2f661c900ce 100644
--- a/regression/cbmc/Quantifiers-if/test.desc
+++ b/regression/cbmc/Quantifiers-if/test.desc
@@ -7,5 +7,5 @@ main.c
 ^\[main.assertion.3\] success 1: SUCCESS$
 ^\[main.assertion.4\] failure 3: FAILURE$
 ^\[main.assertion.5\] success 2: SUCCESS$
-^\*\* 3 of 5 failed \(2 iterations\)$
+^\*\* 3 of 5 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc
index 0f309d9332d..8e38bf5955b 100644
--- a/regression/cbmc/Quantifiers-initialisation2/test.desc
+++ b/regression/cbmc/Quantifiers-initialisation2/test.desc
@@ -7,5 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
 ^\[main.assertion.4\] forall c\[\]: SUCCESS$
 ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
-^\*\* 1 of 5 failed \(2 iterations\)$
+^\*\* 1 of 5 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc
index b22b6666f14..37843fe1472 100644
--- a/regression/cbmc/Quantifiers-not/test.desc
+++ b/regression/cbmc/Quantifiers-not/test.desc
@@ -7,5 +7,5 @@ main.c
 ^\[main.assertion.3\] failure 1: FAILURE$
 ^\[main.assertion.4\] success 3: SUCCESS$
 ^\[main.assertion.5\] failure 2: FAILURE$
-^\*\* 2 of 5 failed \(2 iterations\)$
+^\*\* 2 of 5 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
index a3939c6a78a..d5e98684d0e 100644
--- a/regression/cbmc/Quantifiers-type/test.desc
+++ b/regression/cbmc/Quantifiers-type/test.desc
@@ -4,5 +4,5 @@ main.c
 ^\*\* Results:$
 ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
 ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/fgets1/test.desc b/regression/cbmc/fgets1/test.desc
index 1551462c520..3228a434a07 100644
--- a/regression/cbmc/fgets1/test.desc
+++ b/regression/cbmc/fgets1/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main.assertion.3\] assertion p\[1\]=='b': FAILURE
-\*\* 1 of \d+ failed \(2 iterations\)
+\*\* 1 of \d+ failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
index 218000c3650..f45db0953f4 100644
--- a/regression/cbmc/memory_allocation1/test.desc
+++ b/regression/cbmc/memory_allocation1/test.desc
@@ -7,6 +7,6 @@ main.c
 \[main.assertion.1\] assertion \*p==42: SUCCESS
 \[main.pointer_dereference.14\] dereference failure: pointer invalid in p\[.*1\]: FAILURE
 \[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS
-\*\* 12 of 26 failed \(2 iterations\)
+\*\* 12 of 26 failed
 --
 ^warning: ignoring
diff --git a/regression/cbmc/memset1/test.desc b/regression/cbmc/memset1/test.desc
index aef7e29d151..2473a80a95e 100644
--- a/regression/cbmc/memset1/test.desc
+++ b/regression/cbmc/memset1/test.desc
@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE
-\*\* 1 of 12 failed \(2 iterations\)
+\*\* 1 of 12 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/pipe1/test.desc b/regression/cbmc/pipe1/test.desc
index 26a7b98287a..3c4aa9c5bc4 100644
--- a/regression/cbmc/pipe1/test.desc
+++ b/regression/cbmc/pipe1/test.desc
@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$
-^\*\* 1 of 5 failed \(2 iterations\)$
+^\*\* 1 of 5 failed 
 --
 ^warning: ignoring
diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc
index be81dbdc393..584e452fc11 100644
--- a/regression/cbmc/pointer-function-parameters-2/test.desc
+++ b/regression/cbmc/pointer-function-parameters-2/test.desc
@@ -2,7 +2,6 @@ CORE
 main.c
 --function fun --cover branch
 ^\*\* 7 of 7 covered \(100.0%\)$
-^\*\* Used 4 iterations$
 ^Test suite:$
 ^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
 ^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc
index 89fbd70531a..809730ea5f1 100644
--- a/regression/cbmc/pointer-function-parameters/test.desc
+++ b/regression/cbmc/pointer-function-parameters/test.desc
@@ -2,7 +2,6 @@ CORE
 main.c
 --function fun --cover branch
 ^\*\* 5 of 5 covered \(100\.0%\)$
-^\*\* Used 3 iterations$
 ^Test suite:$
 ^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
 ^a=&tmp\$\d+!0, tmp\$\d+=4$
diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc
index 77f0c2e7eb8..9cdafb87bed 100644
--- a/regression/strings/test_pass1/test.desc
+++ b/regression/strings/test_pass1/test.desc
@@ -5,4 +5,4 @@ test.c
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): SUCCESS
 ^\[main.assertion.2\] assertion !__CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): FAILURE$
-^\*\* 1 of 2 failed \(2 iterations\)$
+^\*\* 1 of 2 failed 
diff --git a/src/Makefile b/src/Makefile
index 3f53a79fc32..365336893c7 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -93,4 +93,17 @@ cprover-jar-build:
 	cd target; jar cf org.cprover.jar `find . -name "*.class"`; \
 	mv org.cprover.jar ../../../)
 
-.PHONY: minisat2-download glucose-download cprover-jar-build
+ipasir-download:
+	# get the 2016 version of the ipasir package, which contains a few solvers
+	@echo "Download ipasir 2016 package"
+	@(lwp-download http://baldur.iti.kit.edu/sat-competition-2016/downloads/ipasir.zip ../ipasir.zip)
+	@(cd ..; unzip -u ipasir.zip)
+
+ipasir-build: ipasir-download
+	# build libpicosat, and create a libipasir.a in ipasir directory
+	# make sure that the ipasir.h file is located there as well (ships with 2016 package)
+	@echo "Build Picosat 961 from ipasir 2016 package"
+	$(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a
+	@(cd ../ipasir; ln -sf sat/picosat961/libipasirpicosat961.a libipasir.a)
+
+.PHONY: ipasir-build minisat2-download glucose-download cprover-jar-build
diff --git a/src/common b/src/common
index ad74f211928..fd093cc69af 100644
--- a/src/common
+++ b/src/common
@@ -155,6 +155,48 @@ else
   $(error Invalid setting for BUILD_ENV: $(BUILD_ENV_))
 endif
 
+# select default solver to be minisat2 if no other is specified
+ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),)
+  MINISAT2 = ../../minisat-2.2.1
+endif
+
+ifneq ($(IPASIR),)
+  CP_CXXFLAGS += -DHAVE_IPASIR
+endif
+
+ifneq ($(PRECOSAT),)
+  CP_CXXFLAGS += -DHAVE_PRECOSAT
+endif
+
+ifneq ($(PICOSAT),)
+  CP_CXXFLAGS += -DHAVE_PICOSAT
+endif
+
+ifneq ($(LINGELING),)
+  CP_CXXFLAGS += -DHAVE_LINGELING
+endif
+
+ifneq ($(CHAFF),)
+  CP_CXXFLAGS += -DHAVE_CHAFF
+endif
+
+ifneq ($(BOOLEFORCE),)
+  CP_CXXFLAGS += -DHAVE_BOOLEFORCE
+endif
+
+ifneq ($(MINISAT),)
+  CP_CXXFLAGS += -DHAVE_MINISAT
+endif
+
+ifneq ($(MINISAT2),)
+  CP_CXXFLAGS += -DHAVE_MINISAT2
+endif
+
+ifneq ($(GLUCOSE),)
+  CP_CXXFLAGS += -DHAVE_GLUCOSE
+endif
+
+
 
 first_target: all
 
diff --git a/src/config.inc b/src/config.inc
index 5c276dc19c6..93b44e39a50 100644
--- a/src/config.inc
+++ b/src/config.inc
@@ -22,10 +22,15 @@ endif
 #CHAFF = ../../zChaff
 #BOOLEFORCE = ../../booleforce-0.4
 #MINISAT = ../../MiniSat-p_v1.14
-MINISAT2 = ../../minisat-2.2.1
+#MINISAT2 = ../../minisat-2.2.1
+#IPASIR = ../../ipasir
 #GLUCOSE = ../../glucose-syrup
 #SMVSAT =
 
+# Extra library for SAT solver. This should link to the archive file to be used
+# when linking against an IPASIR solver.
+LIBSOLVER =
+
 ifneq ($(PRECOSAT),)
   CP_CXXFLAGS += -DSATCHECK_PRECOSAT
 endif
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index a3e7219db4d..c8cbebee1a6 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -21,6 +21,14 @@ ifneq ($(MINISAT2),)
   CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
 endif
 
+ifneq ($(IPASIR),)
+  IPASIR_SRC=sat/satcheck_ipasir.cpp
+  IPASIR_INCLUDE=-I $(IPASIR)
+  IPASIR_LIB=$(IPASIR)/ipasir.a
+  CP_CXXFLAGS += -DHAVE_IPASIR -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
+  override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
+endif
+
 ifneq ($(GLUCOSE),)
   GLUCOSE_SRC=sat/satcheck_glucose.cpp
   GLUCOSE_INCLUDE=-I $(GLUCOSE)
@@ -82,6 +90,7 @@ SRC = $(BOOLEFORCE_SRC) \
       $(GLUCOSE_SRC) \
       $(LINGELING_SRC) \
       $(MINISAT2_SRC) \
+      $(IPASIR_SRC) \
       $(MINISAT_SRC) \
       $(PICOSAT_SRC) \
       $(PRECOSAT_SRC) \
@@ -198,6 +207,7 @@ SRC = $(BOOLEFORCE_SRC) \
 
 INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
+  $(IPASIR_INCLUDE) \
   $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
 	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
 
@@ -222,4 +232,4 @@ endif
 solvers$(LIBEXT): $(OBJ) $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
         $(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
 	$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
-	$(LINKLIB)
+	$(LINKLIB) $(LIBSOLVER)
diff --git a/src/solvers/prop/literal.h b/src/solvers/prop/literal.h
index 24e62ba599a..7e93efe052c 100644
--- a/src/solvers/prop/literal.h
+++ b/src/solvers/prop/literal.h
@@ -193,6 +193,9 @@ inline literalt neg(literalt a) { return !a; }
 inline literalt pos(literalt a) { return a; }
 
 
+inline bool is_false (const literalt &l) { return (l.is_false()); }
+inline bool is_true (const literalt &l) { return (l.is_true()); }
+
 // bit-vectors
 typedef std::vector<literalt> bvt;
 
diff --git a/src/solvers/sat/satcheck.h b/src/solvers/sat/satcheck.h
index 4905f3195ee..cc20e33476a 100644
--- a/src/solvers/sat/satcheck.h
+++ b/src/solvers/sat/satcheck.h
@@ -10,7 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_SAT_SATCHECK_H
 #define CPROVER_SOLVERS_SAT_SATCHECK_H
 
-// this picks the "default" SAT solver
+// This sets a define for the SAT solver
+// based on set flags that come via the compiler
+// command line.
 
 // #define SATCHECK_ZCHAFF
 // #define SATCHECK_MINISAT1
@@ -21,6 +23,42 @@ Author: Daniel Kroening, kroening@kroening.com
 // #define SATCHECK_PICOSAT
 // #define SATCHECK_LINGELING
 
+#if defined(HAVE_IPASIR) && !defined(SATCHECK_IPASIR)
+#define SATCHECK_IPASIR
+#endif
+
+#if defined(HAVE_ZCHAFF) && !defined(SATCHECK_ZCHAFF)
+#define SATCHECK_ZCHAFF
+#endif
+
+#if defined(HAVE_MINISAT1) && !defined(SATCHECK_MINISAT1)
+#define SATCHECK_MINISAT1
+#endif
+
+#if defined(HAVE_MINISAT2) && !defined(SATCHECK_MINISAT2)
+#define SATCHECK_MINISAT2
+#endif
+
+#if defined(HAVE_GLUCOSE) && !defined(SATCHECK_GLUCOSE)
+#define SATCHECK_GLUCOSE
+#endif
+
+#if defined(HAVE_BOOLEFORCE) && !defined(SATCHECK_BOOLEFORCE)
+#define SATCHECK_BOOLEFORCE
+#endif
+
+#if defined(HAVE_PRECOSAT) && !defined(SATCHECK_PRECOSAT)
+#define SATCHECK_PRECOSAT
+#endif
+
+#if defined(HAVE_PICOSAT) && !defined(SATCHECK_PICOSAT)
+#define SATCHECK_PICOSAT
+#endif
+
+#if defined(HAVE_LINGELING) && !defined(SATCHECK_LINGELING)
+#define SATCHECK_LINGELING
+#endif
+
 #if defined SATCHECK_ZCHAFF
 
 #include "satcheck_zchaff.h"
@@ -49,6 +87,13 @@ typedef satcheck_minisat1t satcheck_no_simplifiert;
 typedef satcheck_minisat_simplifiert satcheckt;
 typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert;
 
+#elif defined SATCHECK_IPASIR
+
+#include "satcheck_ipasir.h"
+
+typedef satcheck_ipasirt satcheckt;
+typedef satcheck_ipasirt satcheck_no_simplifiert;
+
 #elif defined SATCHECK_PRECOSAT
 
 #include "satcheck_precosat.h"
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp
new file mode 100644
index 00000000000..6c91de27fa0
--- /dev/null
+++ b/src/solvers/sat/satcheck_ipasir.cpp
@@ -0,0 +1,196 @@
+/*******************************************************************\
+
+Module: External SAT Solver Binding
+
+Author: Norbert Manthey, nmanthey@amazon.com
+
+\*******************************************************************/
+
+#ifndef _MSC_VER
+#include <inttypes.h>
+#endif
+
+#include <algorithm>
+#include <cassert>
+#include <stack>
+
+#include <util/threeval.h>
+
+#include "satcheck_ipasir.h"
+
+#ifdef HAVE_IPASIR
+
+extern "C"
+{
+#include <ipasir.h>
+}
+
+/*
+
+Interface description:
+https://github.com/biotomas/ipasir/blob/master/ipasir.h
+
+Representation:
+Variables for a formula start with 1! 0 is used as termination symbol.
+
+*/
+
+tvt satcheck_ipasirt::l_get(literalt a) const
+{
+  if(a.is_true())
+    return tvt(true);
+  else if(a.is_false())
+    return tvt(false);
+
+  tvt result;
+
+  // compare to internal no_variables number
+  if(a.var_no()>=(unsigned)no_variables())
+    return tvt::unknown();
+
+  const int val=ipasir_val(solver, a.var_no());
+
+  if(val>0)
+    result=tvt(true);
+  else if(val<0)
+    result=tvt(false);
+  else
+    return tvt::unknown();
+
+  if(a.sign())
+    result=!result;
+
+  return result;
+}
+
+const std::string satcheck_ipasirt::solver_text()
+{
+  return std::string(ipasir_signature());
+}
+
+void satcheck_ipasirt::lcnf(const bvt &bv)
+{
+  forall_literals(it, bv)
+  {
+    if(it->is_true())
+      return;
+    else if(!it->is_false())
+      INVARIANT(it->var_no()<(unsigned)no_variables(),
+             "reject out of bound variables");
+  }
+
+  forall_literals(it, bv)
+  {
+    if(!it->is_false())
+    {
+      // add literal with correct sign
+      ipasir_add(solver, it->dimacs());
+    }
+  }
+  ipasir_add(solver, 0); // terminate clause
+
+  clause_counter++;
+}
+
+propt::resultt satcheck_ipasirt::prop_solve()
+{
+  INVARIANT(status!=statust::ERROR, "there cannot be an error");
+
+  {
+    messaget::status() <<
+      (no_variables()-1) << " variables, " <<
+      clause_counter << " clauses" << eom;
+  }
+
+  // use the internal representation, as ipasir does not support reporting the
+  // status
+  if(status==statust::UNSAT)
+  {
+    messaget::status() <<
+      "SAT checker inconsistent: instance is UNSATISFIABLE" << eom;
+  }
+  else
+  {
+    // if assumptions contains false, we need this to be UNSAT
+    bvt::const_iterator it = std::find_if(assumptions.begin(),
+      assumptions.end(), is_false);
+    const bool has_false = it != assumptions.end();
+
+    if(has_false)
+    {
+      messaget::status() <<
+        "got FALSE as assumption: instance is UNSATISFIABLE" << eom;
+    }
+    else
+    {
+      forall_literals(it, assumptions)
+        if(!it->is_false())
+          ipasir_assume(solver, it->dimacs());
+
+      // solve the formula, and handle the return code (10=SAT, 20=UNSAT)
+      int solver_state=ipasir_solve(solver);
+      if(10==solver_state)
+      {
+        messaget::status() <<
+          "SAT checker: instance is SATISFIABLE" << eom;
+        status=statust::SAT;
+        return resultt::P_SATISFIABLE;
+      }
+      else if(20==solver_state)
+      {
+        messaget::status() <<
+          "SAT checker: instance is UNSATISFIABLE" << eom;
+      }
+      else
+      {
+        messaget::status() <<
+          "SAT checker: solving returned without solution" << eom;
+        throw "solving inside IPASIR SAT solver has been interrupted";
+      }
+    }
+  }
+
+  status=statust::UNSAT;
+  return resultt::P_UNSATISFIABLE;
+}
+
+void satcheck_ipasirt::set_assignment(literalt a, bool value)
+{
+  INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
+  INVARIANT(false, "method not supported");
+}
+
+satcheck_ipasirt::satcheck_ipasirt()
+: solver(nullptr)
+{
+  INVARIANT(!solver, "there cannot be a solver already");
+  solver=ipasir_init();
+}
+
+satcheck_ipasirt::~satcheck_ipasirt()
+{
+  if(solver)
+    ipasir_release(solver);
+  solver=nullptr;
+}
+
+bool satcheck_ipasirt::is_in_conflict(literalt a) const
+{
+  return ipasir_failed(solver, a.var_no());
+}
+
+void satcheck_ipasirt::set_assumptions(const bvt &bv)
+{
+  bvt::const_iterator it = std::find_if(bv.begin(), bv.end(), is_true);
+  const bool has_true = it != bv.end();
+
+  if(has_true)
+  {
+    assumptions.clear();
+    return;
+  }
+  // only copy assertions, if there is no false in bt parameter
+  assumptions=bv;
+}
+
+#endif
diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h
new file mode 100644
index 00000000000..0536e535a87
--- /dev/null
+++ b/src/solvers/sat/satcheck_ipasir.h
@@ -0,0 +1,59 @@
+/*******************************************************************\
+
+Module:
+
+Author: Norbert Manthey, nmanthey@amazon.com
+
+Sample compilation command:
+(to be executed from base directory of project)
+
+make clean
+make ipasir-build
+CXXFLAGS=-g IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a \
+  CFLAGS="-Wall -O2 -DSATCHECK_IPSAIR" LINKFLAGS="-static" \
+  make -j 7 -C $(pwd)/src/;
+
+Note: Make sure, the LIBSOLVER variable is set in the environment!
+      The variable should point to the solver you actually want to
+      link against.
+
+\*******************************************************************/
+
+#ifndef CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
+#define CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H
+
+#include "cnf.h"
+
+/// Interface for generic SAT solver interface IPASIR
+class satcheck_ipasirt:public cnf_solvert
+{
+public:
+  satcheck_ipasirt();
+  virtual ~satcheck_ipasirt() override;
+
+  /// This method returns the description produced by the linked SAT solver
+  virtual const std::string solver_text() override;
+
+  virtual resultt prop_solve() override;
+
+  /// This method returns the truth value for a literal of the current SAT model
+  virtual tvt l_get(literalt a) const override final;
+
+  virtual void lcnf(const bvt &bv) override final;
+
+  /* This method is not supported, and currently not called anywhere in CBMC */
+  virtual void set_assignment(literalt a, bool value) override;
+
+  virtual void set_assumptions(const bvt &_assumptions) override;
+
+  virtual bool is_in_conflict(literalt a) const override;
+  virtual bool has_set_assumptions() const override final { return true; }
+  virtual bool has_is_in_conflict() const override final { return true; }
+
+protected:
+  void *solver;
+
+  bvt assumptions;
+};
+
+#endif // CPROVER_SOLVERS_SAT_SATCHECK_IPASIR_H