diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 8b1dda26a5..0be0992a32 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2680,9 +2680,11 @@ struct
             if get_bool "sem.malloc.fail"
             then AD.join addr AD.null_ptr (* calloc can fail and return NULL *)
             else addr in
+          let ik = Cilfacade.ptrdiff_ikind () in
+          let blobsize = ID.mul (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st size) (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st n) in
           (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *)
-          set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.from_var heap_var), TVoid [], `Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (`Blob (VD.bot (), eval_int (Analyses.ask_of_ctx ctx) gs st size, false))));
-                                                         (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), `Address (add_null (AD.from_var_offset (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
+          set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.from_var heap_var), TVoid [], `Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (`Blob (VD.bot (), blobsize, false))));
+                                  (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), `Address (add_null (AD.from_var_offset (heap_var, `Index (IdxDom.of_int  (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))]
         | _ -> st
       end
     | Realloc { ptr = p; size }, _ ->
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index b7bd3c3974..ac75253d34 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -41,7 +41,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 (** Linux kernel functions. *)
 let linux_descs_list: (string * LibraryDesc.t) list = (* LibraryDsl. *) [
 
-  ]
+]
 
 (** Goblint functions. *)
 let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml
index 8f90780fb3..90c167bdad 100644
--- a/src/analyses/mallocWrapperAnalysis.ml
+++ b/src/analyses/mallocWrapperAnalysis.ml
@@ -3,8 +3,10 @@
 open Prelude.Ana
 open Analyses
 open GobConfig
+open ThreadIdDomain
+module Q = Queries
 
-module Spec : Analyses.MCPSpec =
+module Spec: Analyses.MCPSpec =
 struct
   include Analyses.DefaultSpec
 
@@ -13,24 +15,49 @@ struct
       let bot_name = "Unreachable node"
     end)
 
-  module Node = struct
-    include Node
+  module Chain = Lattice.Chain (struct
+      let n () =
+        let p = get_int "ana.malloc.unique_address_count" in
+        if p < 0 then
+          failwith "Option ana.malloc.unique_address_count has to be non-negative"
+        else p + 1 (* Unique addresses + top address *)
+
+      let names x = if x = (n () - 1) then "top" else Format.asprintf "%d" x
+
+    end)
+
+  (* Map for counting malloc node visits up to n (of the current thread). *)
+  module MallocCounter = struct
+    include MapDomain.MapBot_LiftTop(PL)(Chain)
+
+    (* Increase counter for given node. If it does not exists yet, create it. *)
+    let add_malloc counter node =
+      let malloc = `Lifted node in
+      let count = find malloc counter in
+      if Chain.is_top count then
+        counter
+      else
+        remove malloc counter |> add malloc (count + 1)
+  end
+
+  module ThreadNode = struct
+    include Printable.Prod3 (ThreadIdDomain.ThreadLifted) (Node) (Chain)
+
     (* Description that gets appended to the varinfo-name in user output. *)
-    let describe_varinfo (v: varinfo) node =
+    let describe_varinfo (v: varinfo) (t, node, c) =
       let loc = UpdateCil.getLoc node in
       CilType.Location.show loc
 
-    let name_varinfo node = match node with
-      | Node.Statement s -> "(alloc@sid:" ^ (string_of_int s.sid) ^ ")"
-      | _ -> failwith "A function entry or return node can not be the node after a malloc"
+    let name_varinfo (t, node, c) =
+      Format.asprintf "(alloc@sid:%s@tid:%s(#%s))" (Node.show_id node) (ThreadLifted.show t) (Chain.show c)
+
   end
 
-  module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(Node)
+  module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode)
   let name () = "mallocWrapper"
-  module D = PL
-  module C = D
 
-  module Q = Queries
+  module D = Lattice.Prod (MallocCounter) (PL)
+  module C = D
 
   let wrappers = Hashtbl.create 13
 
@@ -48,42 +75,64 @@ struct
     ctx.local
 
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    let calleeofinterest = Hashtbl.mem wrappers f.svar.vname in
-    let calleectx = if calleeofinterest then
-        if ctx.local = `Top then
-          `Lifted ctx.node (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *)
-        else ctx.local (* if an interesting callee is called by an interesting caller, then we remember the caller context *)
-      else D.top () in  (* if an uninteresting callee is called, then we forget what was called before *)
-    [(ctx.local, calleectx)]
-
-  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
-    ctx.local
-
-  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    ctx.local
+    let counter, wrapper_node = ctx.local in
+    let new_wrapper_node =
+      if Hashtbl.mem wrappers f.svar.vname then
+        match wrapper_node with
+        | `Lifted _ ->  wrapper_node (* if an interesting callee is called by an interesting caller, then we remember the caller context *)
+        | _ ->  (`Lifted ctx.node) (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *)
+      else
+        PL.top () (* if an uninteresting callee is called, then we forget what was called before *)
+    in
+    let callee = (counter, new_wrapper_node) in
+    [(ctx.local, callee)]
+
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc ((counter, _):D.t) : D.t =
+    (* Keep (potentially higher) counter from callee and keep wrapper node from caller *)
+    let _, lnode = ctx.local in
+    (counter, lnode)
+
+  let special (ctx: (D.t, G.t, C.t, V.t) ctx) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let desc = LibraryFunctions.find f in
+    match desc.special arglist with
+    | Malloc _ | Calloc _ | Realloc _ ->
+      let counter, wrapper_node = ctx.local in
+      (MallocCounter.add_malloc counter ctx.node, wrapper_node)
+    | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
+
+  let threadenter ctx lval f args =
+    (* The new thread receives a fresh counter *)
+    [D.bot ()]
+
   let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  v = D.top ()
 
   type marshal = NodeVarinfoMap.marshal
 
   let get_heap_var = NodeVarinfoMap.to_varinfo
-  let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Queries.result =
+
+
+  let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Q.result =
+    let counter, wrapper_node = ctx.local in
     match q with
     | Q.HeapVar ->
-      let node = match ctx.local with
-        | `Lifted vinfo -> vinfo
+      let node = match wrapper_node with
+        | `Lifted wrapper_node -> wrapper_node
         | _ -> ctx.node
       in
-      let var = get_heap_var node in
+      let count = MallocCounter.find (`Lifted node) counter in
+      let var = get_heap_var (ctx.ask Q.CurrentThreadId, node, count) in
       var.vdecl <- UpdateCil.getLoc node; (* TODO: does this do anything bad for incremental? *)
       `Lifted var
     | Q.IsHeapVar v ->
       NodeVarinfoMap.mem_varinfo v
     | Q.IsMultiple v ->
-      NodeVarinfoMap.mem_varinfo v
+      begin match NodeVarinfoMap.from_varinfo v with
+        | Some (_, _, c) -> Chain.is_top c || not (ctx.ask Q.MustBeUniqueThread)
+        | None -> false
+      end
     | _ -> Queries.Result.top q
 
   let init marshal =
@@ -95,4 +144,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis (module Spec)
diff --git a/src/cdomains/threadFlagDomain.ml b/src/cdomains/threadFlagDomain.ml
index 8fef40ac7d..09d19d9e74 100644
--- a/src/cdomains/threadFlagDomain.ml
+++ b/src/cdomains/threadFlagDomain.ml
@@ -30,7 +30,7 @@ module Simple: S =
 struct
   module SimpleNames =
   struct
-    let n = 3
+    let n () = 3
     let names = function
       | 0 -> "Singlethreaded"
       | 1 -> "Multithreaded (main)"
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index a18b84d2fc..f5d04b0db7 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -335,7 +335,7 @@ struct
     let one_addr = let open Addr in function
         (* only allow conversion of float pointers if source and target type are the same *)
         | Addr ({ vtype = TFloat(fkind, _); _}, _) as x when (match t with TFloat (fkind', _) when fkind = fkind' -> true | _ -> false) -> x
-          (* do not allow conversion from/to float pointers*)
+        (* do not allow conversion from/to float pointers*)
         | Addr ({ vtype = TFloat(_); _}, _) -> UnknownPtr
         | _ when (match t with TFloat _ -> true | _ -> false) -> UnknownPtr
         | Addr ({ vtype = TVoid _; _} as v, offs) when not (Cilfacade.isCharType t) -> (* we had no information about the type (e.g. malloc), so we add it; ignore for casts to char* since they're special conversions (N1570 6.3.2.3.7) *)
@@ -914,7 +914,22 @@ struct
         begin
           let l', o' = shift_one_over l o in
           let x = zero_init_calloced_memory orig x t in
-          mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
+          (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
+        let do_strong_update =
+            begin match v with
+            | (Var var, _) ->
+              let blob_size_opt = ID.to_int s in
+              not @@ ask.f (Q.IsMultiple var)
+              && not @@ Cil.isVoidType t      (* Size of value is known *)
+              && Option.is_some blob_size_opt (* Size of blob is known *)
+              && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.alignOf_int t)
+            | _ -> false
+            end
+          in
+          if do_strong_update then
+            `Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
+          else
+            mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
         end
       | `Thread _, _ ->
         (* hack for pthread_t variables *)
diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml
index c6920d9e3f..09f52bb8a3 100644
--- a/src/domains/lattice.ml
+++ b/src/domains/lattice.ml
@@ -580,8 +580,8 @@ struct
 
   let bot () = 0
   let is_bot x = x = 0
-  let top () = P.n - 1
-  let is_top x = x = P.n - 1
+  let top () = P.n () - 1
+  let is_top x = x = P.n () - 1
 
   let leq x y = x <= y
   let join x y = max x y
diff --git a/src/domains/printable.ml b/src/domains/printable.ml
index a67bee25c8..77e65f3de3 100644
--- a/src/domains/printable.ml
+++ b/src/domains/printable.ml
@@ -463,7 +463,7 @@ struct
 end
 
 module type ChainParams = sig
-  val n: int
+  val n: unit -> int
   val names: int -> string
 end
 
@@ -477,7 +477,7 @@ struct
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (P.names x)
   let to_yojson x = `String (P.names x)
 
-  let arbitrary () = QCheck.int_range 0 (P.n - 1)
+  let arbitrary () = QCheck.int_range 0 (P.n () - 1)
   let relift x = x
 end
 
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index b0a0ce17cb..22fb82f6a8 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -749,6 +749,12 @@
                 "kmalloc", "__kmalloc", "usb_alloc_urb", "__builtin_alloca",
                 "kzalloc"
               ]
+            },
+            "unique_address_count": {
+                "title": "ana.malloc.unique_address_count",
+                "description": "Number of unique memory addresses allocated for each malloc node.",
+                "type": "integer",
+                "default": 0
             }
           },
           "additionalProperties": false
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index 8837d9fe6c..ec39fd9020 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -24,7 +24,7 @@ struct
   module ChainParams =
   struct
     (* let n = List.length Arg.path *)
-    let n = -1
+    let n () = -1
     let names x = "state " ^ string_of_int x
   end
   module D = Lattice.Flat (Printable.Chain (ChainParams)) (Printable.DefaultNames)
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 03885a31fe..028f99e65d 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -194,7 +194,7 @@ struct
 
   module ChainParams =
   struct
-    let n = max_result - 1
+    let n () = max_result - 1
     let names i = show_result (Option.get (result_of_enum i))
   end
   include Lattice.Chain (ChainParams)
diff --git a/tests/regression/11-heap/04-malloc_unique_addresses.c b/tests/regression/11-heap/04-malloc_unique_addresses.c
new file mode 100644
index 0000000000..3e004f1dfc
--- /dev/null
+++ b/tests/regression/11-heap/04-malloc_unique_addresses.c
@@ -0,0 +1,28 @@
+// PARAM: --set ana.malloc.unique_address_count 2
+
+// Copied from 29/07. Here, unique addresses are allocated for both x and y.
+// Therefore, it is not necessary to specify wrapper function.
+
+#include <stdlib.h>
+#include <stdint.h>
+#include <assert.h>
+
+void* myalloc(size_t s) {
+    return malloc(s);
+}
+
+int main() {
+  int* x = myalloc(sizeof(int));
+  int* y = myalloc(sizeof(int));
+  int *p;
+
+  *x = 0;
+  *y = 1;
+
+  assert(*x == 0);
+  assert(*y == 1);
+
+  p = x; x = y; y = p;
+  assert(*x == 1);
+  assert(*y == 0);
+}
diff --git a/tests/regression/11-heap/05-malloc_not_unique_address.c b/tests/regression/11-heap/05-malloc_not_unique_address.c
new file mode 100644
index 0000000000..581744f49c
--- /dev/null
+++ b/tests/regression/11-heap/05-malloc_not_unique_address.c
@@ -0,0 +1,24 @@
+// PARAM: --set ana.malloc.unique_address_count 1
+
+// Copied from 11/05. Here, malloc will allocate an unique address for x only.
+
+#include <stdlib.h>
+#include <stdint.h>
+#include <assert.h>
+
+void* myalloc(size_t s) {
+    return malloc(s);
+}
+
+int main() {
+  int* x = myalloc(sizeof(int));
+  int* y = myalloc(sizeof(int));
+  int* z = myalloc(sizeof(int));
+
+  *x = 0;
+  *y = 1;
+  *z = 0;
+
+  assert(*x == 0);
+  assert(*y == 1); // UNKNOWN!
+}
diff --git a/tests/regression/11-heap/06-wrapper_plus_unique_addresses.c b/tests/regression/11-heap/06-wrapper_plus_unique_addresses.c
new file mode 100644
index 0000000000..f96dd1b9da
--- /dev/null
+++ b/tests/regression/11-heap/06-wrapper_plus_unique_addresses.c
@@ -0,0 +1,34 @@
+// PARAM: --set ana.malloc.wrappers "['myalloc2']" --set ana.malloc.unique_address_count 2
+
+
+// Copied from 02/21. Here, only the inner wrapper function is specified. This should tests
+// the combination of uniqueness analysis and malloc wrapper analysis.
+
+#include <stdlib.h>
+#include <assert.h>
+
+void *myalloc(size_t n) {
+  return malloc(n);
+}
+
+void *myalloc2(size_t n) {
+  return myalloc(n);
+}
+
+int main() {
+  int *x = myalloc2(sizeof(int));
+  int *y = myalloc2(sizeof(int));
+  int *p;
+
+  *x = 0;
+  *y = 1;
+
+  assert(*x == 0);
+  assert(*y == 1);
+
+  p = x; x = y; y = p;
+  assert(*x == 1);
+  assert(*y == 0);
+
+  return 0;
+}
diff --git a/tests/regression/11-heap/07-strong_updates.c b/tests/regression/11-heap/07-strong_updates.c
new file mode 100644
index 0000000000..d18b35d1cf
--- /dev/null
+++ b/tests/regression/11-heap/07-strong_updates.c
@@ -0,0 +1,25 @@
+// PARAM: --set ana.malloc.unique_address_count 2
+
+// Both variables x and y are unique and can be strongly (destructively) updated.
+
+#include <assert.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+void* myalloc(size_t s) {
+    return malloc(s);
+}
+
+int main() {
+  int* x = myalloc(sizeof(int));
+  int* y = myalloc(sizeof(int));
+
+  *x = 0;
+  *y = 1;
+
+  *x = 2;
+  *y = 3;
+
+  assert (*x == 2);
+  assert (*y == 3);
+}
diff --git a/tests/regression/11-heap/08-no_strong_update.c b/tests/regression/11-heap/08-no_strong_update.c
new file mode 100644
index 0000000000..ee1b8c5612
--- /dev/null
+++ b/tests/regression/11-heap/08-no_strong_update.c
@@ -0,0 +1,26 @@
+// PARAM: --set ana.malloc.unique_address_count 1
+
+// Copied from 11/05. Here, variable y is not unique and cannot be strongly updated.
+
+#include <stdlib.h>
+#include <stdint.h>
+#include <assert.h>
+
+void* myalloc(size_t s) {
+    return malloc(s);
+}
+
+int main() {
+  int* x = myalloc(sizeof(int));
+  int* y = myalloc(sizeof(int));
+  int *p;
+
+  *x = 0;
+  *y = 1;
+
+  *x = 2;
+  *y = 3;
+
+  assert (*x == 2);
+  assert (*y == 3); // UNKNOWN!
+}
diff --git a/tests/regression/11-heap/09-no_strong_update_not_unique_thread.c b/tests/regression/11-heap/09-no_strong_update_not_unique_thread.c
new file mode 100644
index 0000000000..025e219b26
--- /dev/null
+++ b/tests/regression/11-heap/09-no_strong_update_not_unique_thread.c
@@ -0,0 +1,33 @@
+// PARAM: --set ana.malloc.unique_address_count 2
+
+// Strong updates are not possible in thread because it is not unique.
+
+#include <assert.h>
+#include <stdlib.h>
+#include <pthread.h>
+
+void *thread(void *v)
+{
+    int *x = malloc(sizeof(int));
+    int *y = malloc(sizeof(int));
+
+    *x = 0;
+    *y = 1;
+
+    *x = 2;
+    *y = 3;
+
+    assert (*x == 2); // UNKNOWN!
+    assert (*y == 3); // UNKNOWN!
+}
+
+int main(int argc, char **argv)
+{
+	pthread_t tids[argc];
+
+    for (int i = 0; i < argc; i++)
+        pthread_create(&tids[i], NULL, thread, NULL);
+
+    for (int i = 0; i < argc; i++)
+        pthread_join(tids[i], NULL);
+}
diff --git a/tests/regression/11-heap/10-no_strong_update_different_size.c b/tests/regression/11-heap/10-no_strong_update_different_size.c
new file mode 100644
index 0000000000..6ddde7d013
--- /dev/null
+++ b/tests/regression/11-heap/10-no_strong_update_different_size.c
@@ -0,0 +1,20 @@
+// PARAM: --set ana.malloc.unique_address_count 2
+
+#include <assert.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+void* myalloc(size_t s) {
+    return malloc(s);
+}
+
+int main() {
+  int *x = myalloc(2 * sizeof(int));
+  int *y = myalloc(2 * sizeof(int));
+
+  *x = 0;
+  *y = 1;
+  *x = 2; // Size of written value is shorter than blob
+
+  assert (*x == 2); // UNKNOWN!
+}
diff --git a/tests/regression/11-heap/11-threads_malloc_no_race.c b/tests/regression/11-heap/11-threads_malloc_no_race.c
new file mode 100644
index 0000000000..2750cb640b
--- /dev/null
+++ b/tests/regression/11-heap/11-threads_malloc_no_race.c
@@ -0,0 +1,35 @@
+// No race should be reported because thread1 and thread2 are both unique
+// and work with their own allocated memory
+
+#include <stdlib.h>
+#include <pthread.h>
+
+int *f()
+{
+    int *x = malloc(sizeof(int));
+    return x;
+}
+
+void *thread1(void *v)
+{
+    int *x = f();
+    (*x)++; // NORACE
+}
+
+void *thread2(void *v)
+{
+    int *x = f();
+    (*x)++; // NORACE
+}
+
+int main(int argc, char **argv)
+{
+	pthread_t tid1;
+	pthread_t tid2;
+
+    pthread_create(&tid1, NULL, thread1, NULL);
+    pthread_create(&tid2, NULL, thread2, NULL);
+
+    pthread_join(tid1, NULL);
+    pthread_join(tid2, NULL);
+}
diff --git a/tests/regression/11-heap/12-calloc.c b/tests/regression/11-heap/12-calloc.c
new file mode 100644
index 0000000000..db1b21d5a5
--- /dev/null
+++ b/tests/regression/11-heap/12-calloc.c
@@ -0,0 +1,8 @@
+// PARAM: --set ana.malloc.unique_address_count 1
+#include<assert.h>
+#include<stdlib.h>
+int main() {
+  int* arr = calloc(5,sizeof(int));
+  arr[0] = 3;
+  assert(arr[2] == 0); //UNKNOWN
+}
diff --git a/tests/regression/11-heap/13-linear-search.c b/tests/regression/11-heap/13-linear-search.c
new file mode 100644
index 0000000000..21974935c7
--- /dev/null
+++ b/tests/regression/11-heap/13-linear-search.c
@@ -0,0 +1,31 @@
+// PARAM: --set ana.malloc.unique_address_count 3  --enable ana.sv-comp.functions
+#include <assert.h>
+extern void *calloc(unsigned int num, unsigned int size);
+
+void __VERIFIER_as(int cond) {
+  if (!(cond)) {
+    assert(1); // reachable
+  }
+  return;
+}
+unsigned int __VERIFIER_nondet_uint();
+unsigned int  SIZE;
+const unsigned int MAX = 100000;
+int linear_search(int *a, int n, int q) {
+  unsigned int j=0;
+  while (j<n && a[j]!=q) {
+  j++;
+  if (j==20) j=-1;
+  }
+  if (j<SIZE) return 1;
+  else return 0;
+}
+int main() {
+  SIZE=(__VERIFIER_nondet_uint()/2)+1;
+
+  if (SIZE > 1 && SIZE < MAX) {
+    int *a = calloc(SIZE,sizeof(int));
+    a[SIZE/2]=3;
+    __VERIFIER_as(linear_search(a,SIZE,3));
+  }
+}
diff --git a/tests/regression/22-partitioned_arrays/17-large_arrays.c b/tests/regression/22-partitioned_arrays/17-large_arrays.c
index fc29839a36..c449a8ec91 100644
--- a/tests/regression/22-partitioned_arrays/17-large_arrays.c
+++ b/tests/regression/22-partitioned_arrays/17-large_arrays.c
@@ -5,7 +5,7 @@
 #include <stdio.h>
 #include <stddef.h>
 
-// Test to check whether partitioned arrays can have an index expression evaluating to values largers than the max value of int64
+// Test to check whether partitioned arrays can have an index expression evaluating to values larger than the max value of int64
 
 #define LENGTH (LONG_MAX - 600)
 #define STOP (LENGTH - 1)
diff --git a/unittest/cdomains/floatDomainTest.ml b/unittest/cdomains/floatDomainTest.ml
index c13a757722..cf9c6092e3 100644
--- a/unittest/cdomains/floatDomainTest.ml
+++ b/unittest/cdomains/floatDomainTest.ml
@@ -1,43 +1,43 @@
 open OUnit2
 open FloatOps
-
+
 module FloatInterval(Float_t: CFloatType)(Domain_t: FloatDomain.FloatDomainBase) =
 struct
   module FI = Domain_t
   module IT = IntDomain.IntDomTuple
-
+
   let to_float = Float_t.to_float
   let of_float = Float_t.of_float
   let add = Float_t.add
   let sub = Float_t.sub
   let mul = Float_t.mul
   let div = Float_t.div
-
+
   let pred x = Option.get (to_float (Float_t.pred (of_float Nearest x)))
   let succ x = Option.get (to_float (Float_t.succ (of_float Nearest x)))
-
+
   let fmax = Option.get (to_float Float_t.upper_bound)
   let fmin = Option.get (to_float Float_t.lower_bound)
   let fsmall = Option.get (to_float Float_t.smallest)
-
+
   let fi_zero = FI.of_const 0.
   let fi_one = FI.of_const 1.
   let fi_neg_one = FI.of_const (-.1.)
   let itb_true = IT.of_int IBool (Big_int_Z.big_int_of_int 1)
   let itb_false = IT.of_int IBool (Big_int_Z.big_int_of_int 0)
   let itb_unknown = IT.of_interval IBool (Big_int_Z.big_int_of_int 0, Big_int_Z.big_int_of_int 1)
-
+
   let assert_equal v1 v2 =
     assert_equal ~cmp:FI.equal ~printer:FI.show v1 v2
-
+
   let itb_xor v1 v2 = (**returns true, if both IntDomainTuple bool results are either unknown or different *)
     ((IT.equal v1 itb_unknown) && (IT.equal v2 itb_unknown)) || ((IT.equal v1 itb_true) && (IT.equal v2 itb_false)) || ((IT.equal v1 itb_false) && (IT.equal v2 itb_true))
-
+
   (**interval tests *)
   let test_FI_nan _ = 
     assert_equal (FI.top ()) (FI.of_const Float.nan)
-
-
+
+
   let test_FI_add_specific _ =
     let (+) = FI.add in
     let (=) a b = assert_equal b a in
@@ -56,7 +56,7 @@ struct
       (FI.of_interval (1., 2.)) + (FI.of_interval (2., 3.)) = FI.of_interval (3., 5.);
       (FI.of_interval (-. 2., 3.)) + (FI.of_interval (-. 100., 20.)) = FI.of_interval (-. 102., 23.);
     end
-
+
   let test_FI_sub_specific _ =
     let (-) = FI.sub in
     let (=) a b = assert_equal b a in
@@ -74,7 +74,7 @@ struct
       (FI.of_interval (-. 2., 3.)) - (FI.of_interval (-. 100., 20.)) = FI.of_interval (-. 22., 103.);
       (FI.of_const (-. 0.)) - fi_zero = fi_zero
     end
-
+
   let test_FI_mul_specific _ = 
     let ( * ) = FI.mul in
     let (=) a b = assert_equal b a in
@@ -90,14 +90,14 @@ struct
       (FI.of_const fmax) * fi_one = FI.of_const fmax;
       (FI.of_const 2.) * (FI.of_const 0.5) = fi_one;
       (FI.of_interval (-. 2., 3.)) * (FI.of_interval (-. 100., 20.)) = FI.of_interval (-. 300., 200.);
-
+
       let up = if Float_t.name <> "float" then succ 1.00000000000000222 else succ (succ 1.00000000000000111 *. succ 1.00000000000000111) in
       begin
         (FI.of_const 1.00000000000000111) * (FI.of_const 1.00000000000000111) = FI.of_interval (1.00000000000000222 , up);
         (FI.of_const (-. 1.00000000000000111)) * (FI.of_const 1.00000000000000111) = FI.of_interval (-. up, -. 1.00000000000000222)
       end
     end
-
+
   let test_FI_div_specific _ =
     let (/) = FI.div in
     let (=) a b = assert_equal b a in
@@ -117,11 +117,11 @@ struct
       (FI.of_const 4.) / (FI.of_const 2.) = (FI.of_const 2.);
       (FI.of_interval (-. 2., 3.)) / (FI.of_interval (-. 100., 20.)) = FI.top ();
       (FI.of_interval (6., 10.)) / (FI.of_interval (2., 3.)) = (FI.of_interval (2., 5.));
-
+
       (FI.of_const 1.) / (FI.of_const 3.) = (FI.of_interval (pred 0.333333333333333370340767487505, 0.333333333333333370340767487505));
       (FI.of_const (-. 1.)) / (FI.of_const 3.) = (FI.of_interval (-. 0.333333333333333370340767487505, succ (-. 0.333333333333333370340767487505)))
     end
-
+
   let test_FI_casti2f_specific _ =
     let cast_bool a b = 
       assert_equal b (FI.of_int (IT.of_int IBool (Big_int_Z.big_int_of_int a))) in
@@ -142,7 +142,7 @@ struct
       cast (IT.of_interval IInt (Big_int_Z.big_int_of_int (- 100), Big_int_Z.big_int_of_int 100)) (FI.of_interval (-. 100., 100.));
       cast (IT.of_interval IUShort (Big_int_Z.big_int_of_int 2, Big_int_Z.big_int_of_int 100)) (FI.of_interval (2., 100.));
       cast (IT.of_interval IShort (Big_int_Z.big_int_of_int (- 100), Big_int_Z.big_int_of_int 100)) (FI.of_interval (-. 100., 100.));
-
+
       cast (IT.of_interval IULong (Big_int_Z.zero_big_int, Big_int_Z.big_int_of_int64 Int64.max_int)) (FI.of_interval (0., 9223372036854775807.));
       cast (IT.of_interval IULong (Big_int_Z.zero_big_int, Big_int_Z.big_int_of_int64 (9223372036854775806L))) (FI.of_interval (0., 9223372036854775807.));
       cast (IT.of_interval ILong (Big_int_Z.big_int_of_int64 Int64.min_int, Big_int_Z.zero_big_int)) (FI.of_interval (-. 9223372036854775808., 0.));
@@ -153,7 +153,7 @@ struct
       cast (IT.of_interval ILongLong (Big_int_Z.big_int_of_int (- 100), Big_int_Z.big_int_of_int 100)) (FI.of_interval (-. 100., 100.));
       GobConfig.set_bool "ana.int.interval" false;
     end
-
+
   let test_FI_castf2i_specific _ =
     let cast ikind a b = 
       OUnit2.assert_equal ~cmp:IT.equal ~printer:IT.show b (FI.to_int ikind a) in
@@ -166,14 +166,14 @@ struct
       cast IBool (FI.of_interval (-9999999999.,9999999999.)) (IT.top_of IBool);
       cast IBool fi_one (IT.of_bool IBool true);
       cast IBool fi_zero (IT.of_bool IBool false);
-
+
       cast IUChar (FI.of_interval (0.123, 128.999)) (IT.of_interval IUChar (Big_int_Z.big_int_of_int 0, Big_int_Z.big_int_of_int 128));
       cast IChar (FI.of_interval (-. 8.0000000, 127.)) (IT.of_interval IChar (Big_int_Z.big_int_of_int (-8), Big_int_Z.big_int_of_int 127));
       cast IUInt (FI.of_interval (2., 100.)) (IT.of_interval IUInt (Big_int_Z.big_int_of_int 2, Big_int_Z.big_int_of_int 100));
       cast IInt (FI.of_interval (-. 100.2, 100.1)) (IT.of_interval IInt (Big_int_Z.big_int_of_int (- 100), Big_int_Z.big_int_of_int 100));
       cast IUShort (FI.of_interval (2., 100.)) (IT.of_interval IUShort (Big_int_Z.big_int_of_int 2, Big_int_Z.big_int_of_int 100));
       cast IShort (FI.of_interval (-. 100., 100.)) (IT.of_interval IShort (Big_int_Z.big_int_of_int (- 100), Big_int_Z.big_int_of_int 100));
-
+
       cast IULong (FI.of_interval (0., 9223372036854775808.)) (IT.of_interval IULong (Big_int_Z.zero_big_int, Big_int_Z.big_int_of_string "9223372036854775808"));
       cast ILong (FI.of_interval (-. 9223372036854775808., 0.)) (IT.of_interval ILong (Big_int_Z.big_int_of_string "-9223372036854775808", Big_int_Z.zero_big_int));
       cast ILong (FI.of_interval (-. 100.99999, 100.99999)) (IT.of_interval ILong (Big_int_Z.big_int_of_int (- 100), Big_int_Z.big_int_of_int 100));
@@ -182,7 +182,7 @@ struct
       cast ILongLong  (FI.of_interval (-. 100., 100.)) (IT.of_interval ILongLong (Big_int_Z.big_int_of_int (- 100), Big_int_Z.big_int_of_int 100));
       GobConfig.set_bool "ana.int.interval" false;
     end
-
+
   let test_FI_meet_specific _ = 
     let check_meet a b c = 
       assert_equal c (FI.meet a b) in
@@ -192,7 +192,7 @@ struct
       check_meet fi_zero fi_one (FI.bot ());
       check_meet (FI.of_interval (0., 10.)) (FI.of_interval (5., 20.)) (FI.of_interval (5., 10.));
     end
-
+
   let test_FI_join_specific _ =
     let check_join a b c = 
       assert_equal c (FI.join a b) in
@@ -201,7 +201,7 @@ struct
       check_join (FI.top ()) fi_one (FI.top ());
       check_join (FI.of_interval (0., 10.)) (FI.of_interval (5., 20.)) (FI.of_interval (0., 20.));
     end
-
+
   let test_FI_leq_specific _ =
     let check_leq flag a b = 
       OUnit2.assert_equal flag (FI.leq a b) in
@@ -214,7 +214,7 @@ struct
       check_leq true (FI.of_interval (1., 19.)) (FI.of_interval (0., 20.));
       check_leq false (FI.of_interval (0., 20.)) (FI.of_interval (20.0001, 20.0002));
     end
-
+
   let test_FI_widen_specific _ =
     let check_widen a b c = 
       assert_equal c (FI.widen a b) in
@@ -226,7 +226,7 @@ struct
       check_widen fi_one fi_zero (FI.of_interval (fmin, 1.));
       check_widen fi_one (FI.of_interval (0., 2.)) (FI.of_interval (fmin, fmax));
     end
-
+
   let test_FI_narrow_specific _ =
     let check_narrow a b c = 
       assert_equal c (FI.narrow a b) in
@@ -236,7 +236,7 @@ struct
       check_narrow (FI.top ()) fi_zero fi_zero;
       check_narrow fi_zero fi_one fi_zero;
     end
-
+
   let test_FI_ArithmeticOnFloatBot _ =
     begin
       assert_raises (FloatDomain.ArithmeticOnFloatBot ("minimal "^(FI.show (FI.bot ())))) (fun() -> (FI.minimal (FI.bot ())));
@@ -245,62 +245,62 @@ struct
       assert_raises (FloatDomain.ArithmeticOnFloatBot ((FI.show (FI.bot ()))^" op "^(FI.show fi_zero))) (fun() -> (FI.lt (FI.bot ()) fi_zero));
       assert_raises (FloatDomain.ArithmeticOnFloatBot ("unop "^(FI.show (FI.bot ())))) (fun() -> (FI.acos (FI.bot ())));
     end
-
+
   (**interval tests using QCheck arbitraries *)
   let test_FI_not_bot =
     QCheck.Test.make ~name:"test_FI_not_bot" (FI.arbitrary ()) (fun arg -> 
         not (FI.is_bot arg))
-
+
   let test_FI_of_const_not_bot =
     QCheck.Test.make ~name:"test_FI_of_const_not_bot" QCheck.float (fun arg -> 
         not (FI.is_bot (FI.of_const arg)))
-
+
   let test_FI_div_zero_result_top =
     QCheck.Test.make ~name:"test_FI_div_zero_result_top" (FI.arbitrary ()) (fun arg ->
         FI.is_top (FI.div arg (FI.of_const 0.)))
-
+
   let test_FI_accurate_neg =
     QCheck.Test.make ~name:"test_FI_accurate_neg" QCheck.float (fun arg ->
         FI.equal (FI.of_const (-.arg)) (FI.neg (FI.of_const arg)))
-
+
   let test_FI_lt_xor_ge =
     QCheck.Test.make ~name:"test_FI_lt_xor_ge" (QCheck.pair (FI.arbitrary ()) (FI.arbitrary ())) (fun (arg1, arg2) ->
         itb_xor (FI.lt arg1 arg2) (FI.ge arg1 arg2))
-
+
   let test_FI_gt_xor_le =
     QCheck.Test.make ~name:"test_FI_lt_xor_ge" (QCheck.pair (FI.arbitrary ()) (FI.arbitrary ())) (fun (arg1, arg2) ->
         itb_xor (FI.gt arg1 arg2) (FI.le arg1 arg2))
-
+
   let test_FI_eq_xor_ne =
     QCheck.Test.make ~name:"test_FI_lt_xor_ge" (QCheck.pair (FI.arbitrary ()) (FI.arbitrary ())) (fun (arg1, arg2) ->
         itb_xor (FI.eq arg1 arg2) (FI.ne arg1 arg2))
-
+
   let test_FI_add =
     QCheck.Test.make ~name:"test_FI_add" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) ->
         let result = FI.add (FI.of_const arg1) (FI.of_const arg2) in
         (FI.leq (FI.of_const (Option.get (to_float (add Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) && 
         (FI.leq (FI.of_const (Option.get (to_float (add Down (of_float Nearest arg1) (of_float Nearest arg2))))) result))
-
+
   let test_FI_sub =
     QCheck.Test.make ~name:"test_FI_sub" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) ->
         let result = FI.sub (FI.of_const arg1) (FI.of_const arg2) in
         (FI.leq (FI.of_const (Option.get (to_float (sub Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) && 
         (FI.leq (FI.of_const (Option.get (to_float (sub Down (of_float Nearest arg1) (of_float Nearest arg2))))) result))
-
+
   let test_FI_mul =
     QCheck.Test.make ~name:"test_FI_mul" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) ->
         let result = FI.mul (FI.of_const arg1) (FI.of_const arg2) in
         (FI.leq (FI.of_const (Option.get (to_float (mul Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) && 
         (FI.leq (FI.of_const (Option.get (to_float (mul Down (of_float Nearest arg1) (of_float Nearest arg2))))) result))
-
-
+
+
   let test_FI_div =
     QCheck.Test.make ~name:"test_FI_div" (QCheck.pair QCheck.float QCheck.float) (fun (arg1, arg2) ->
         let result = FI.div (FI.of_const arg1) (FI.of_const arg2) in
         (FI.leq (FI.of_const (Option.get (to_float (div Up (of_float Nearest arg1) (of_float Nearest arg2))))) result) && 
         (FI.leq (FI.of_const (Option.get (to_float (div Down (of_float Nearest arg1) (of_float Nearest arg2))))) result))
-
-
+
+
   let test () = [
     "test_FI_nan" >:: test_FI_nan;
     "test_FI_add_specific" >:: test_FI_add_specific;
@@ -317,7 +317,7 @@ struct
     "test_FI_narrow_specific" >:: test_FI_narrow_specific;
     "test_FI_ArithmeticOnFloatBot" >:: test_FI_ArithmeticOnFloatBot;
   ]
-
+
   let test_qcheck () = QCheck_ounit.to_ounit2_test_list [
       test_FI_not_bot;
       test_FI_of_const_not_bot;
@@ -332,10 +332,10 @@ struct
       test_FI_div;
     ]
 end
-
+
 module FloatIntervalTest32 = FloatInterval(CFloat)(FloatDomain.F32Interval)
 module FloatIntervalTest64 = FloatInterval(CDouble)(FloatDomain.F64Interval)
-
+
 let test () = 
   "floatDomainTest" >:::
   [ 
@@ -344,4 +344,4 @@ let test () =
     "float_interval64" >::: FloatIntervalTest64.test ();
     "float_interval_qcheck64" >::: FloatIntervalTest64.test_qcheck ();
   ]
-
+