diff --git a/modules/io/src/lib.zz b/modules/io/src/lib.zz
index 698817e..8f655a7 100644
--- a/modules/io/src/lib.zz
+++ b/modules/io/src/lib.zz
@@ -279,8 +279,7 @@ export fn await(Async mut* self, err::Err+et mut*e, void *poll, void mut* user,
     where safe(poll)
 {
     let mut tt = timeout(self, e,timeout_);
-    string::String+8 mut b;
-    b.clear();
+    string::String+8 mut b = {0};
     if err::check(e) {return;}
 
     poll_fn fp = (poll_fn)poll;
diff --git a/modules/io/src/main.zz b/modules/io/src/main.zz
index 2364b6a..f394def 100644
--- a/modules/io/src/main.zz
+++ b/modules/io/src/main.zz
@@ -25,8 +25,7 @@ export fn main() -> int {
     assert(t.valid());
 
     for (;;) {
-        string::String+20 mut buf2;
-        buf2.clear();
+        string::String+20 mut buf2 = {0};
 
         switch t.read(&e, &buf2) {
             io::Result::Ready => {
@@ -45,8 +44,7 @@ export fn main() -> int {
         }
         e.abort();
 
-        string::String+2 mut buf;
-        buf.clear();
+        string::String+2 mut buf = {0};
 
         switch i.read(&e, &buf) {
             io::Result::Ready => {
diff --git a/modules/pool/src/lib.zz b/modules/pool/src/lib.zz
index 586c17d..636f089 100644
--- a/modules/pool/src/lib.zz
+++ b/modules/pool/src/lib.zz
@@ -149,8 +149,8 @@ export fn free(Pool mut *self, void * unsafe mut ptr_)
         return;
     }
 
-    u8 mut blocks;
-    usize mut startblock;
+    u8 mut blocks = 1;
+    usize mut startblock = 0;
     unsafe {
         ptr = ptr - 8;
         ASAN_UNPOISON_MEMORY_REGION(ptr, 8);
diff --git a/modules/string/src/lib.zz b/modules/string/src/lib.zz
index e84b6e8..264a7e3 100644
--- a/modules/string/src/lib.zz
+++ b/modules/string/src/lib.zz
@@ -57,6 +57,16 @@ export fn append_slice(String+tail mut * self) -> MutSlice
     };
 }
 
+export fn new(String+tail mut * self)
+    model self->len  == 0
+    model nullterm(self->mem)
+{
+    c_string::memset(self->mem, 0, tail);
+    self->len = 0;
+
+    static_attest(nullterm(self->mem));
+}
+
 export fn clear(String+tail mut * self)
     model self->len  == 0
     model nullterm(self->mem)
diff --git a/modules/string/tests/format.zz b/modules/string/tests/format.zz
index e486879..f0e5af2 100644
--- a/modules/string/tests/format.zz
+++ b/modules/string/tests/format.zz
@@ -9,8 +9,7 @@ test blah {
 }
 
 export fn main() -> int {
-    string::String+10 mut s;
-    string::clear(&s);
+    string::String+10 mut s = {0};
 
     string::append_cstr(&s, "hello");
     string::format(&s, "%d%d%d%d", 2, 3, 66,9);
diff --git a/modules/string/tests/split.zz b/modules/string/tests/split.zz
index 4dfcfba..172c4a2 100644
--- a/modules/string/tests/split.zz
+++ b/modules/string/tests/split.zz
@@ -30,14 +30,12 @@ test test5 {
 
 export fn main() -> int {
 
-    string::String+100 mut a;
-    string::clear(&a);
+    string::String+100 mut a = {0};
     string::fgets(&a, stdin);
 
 
     usize mut iterator = 0;
-    string::String+100 mut part;
-    string::clear(&part);
+    string::String+100 mut part = {0};
     while (string::split(&a, ':', &iterator, &part)) {
         printf(">%.*s<\n", (int)part.len, part.mem);
         string::clear(&part);
diff --git a/modules/string/tests/substr.zz b/modules/string/tests/substr.zz
index e30ddfe..5d9a02a 100644
--- a/modules/string/tests/substr.zz
+++ b/modules/string/tests/substr.zz
@@ -41,8 +41,7 @@ test t7{
 
 
 export fn main() -> int {
-    string::String+20 mut sub;
-    string::clear(&sub);
+    string::String+20 mut sub = {0};
 
     char mut * mut line = 0;
     usize mut l = 0;
@@ -53,8 +52,7 @@ export fn main() -> int {
     string::append_bytes(&sub, (u8*)line, (usize)nread -1);
 
 
-    string::String+20 mut s;
-    string::clear(&s);
+    string::String+20 mut s = {0};
 
     nread = as<int>(getline(&line, &l, stdin));
     if nread < 1 { return 1; }
diff --git a/src/smt.rs b/src/smt.rs
index 367304f..17b1144 100644
--- a/src/smt.rs
+++ b/src/smt.rs
@@ -251,9 +251,9 @@ impl Solver {
         self.checkpoint();
     }
 
-    pub fn literal(&mut self, tmp: Symbol, val: u64, typ: Type) {
+    pub fn literal(&mut self, tmp: TemporalSymbol, val: u64, typ: Type) {
 
-        let smt_lhs = self.var(&(tmp,0));
+        let smt_lhs = self.var(&tmp);
 
         match typ {
             Type::Unsigned(size) | Type::Signed(size) => {
diff --git a/src/symbolic.rs b/src/symbolic.rs
index ed3d747..cc55a9d 100644
--- a/src/symbolic.rs
+++ b/src/symbolic.rs
@@ -50,6 +50,7 @@ enum Value{
     Array {
         len:    usize,
         array:  HashMap<usize, Symbol>,
+        null_initialized: bool,
     },
     Unconstrained(String),
     Integer(u64),
@@ -334,6 +335,7 @@ impl Symbolic {
                             self.memory[sym].value = Value::Array {
                                 len:    val as usize,
                                 array:  HashMap::new(),
+                                null_initialized: false,
                             };
                             self.len_into_ssa(sym, expr.loc(), val as usize)?;
 
@@ -341,6 +343,7 @@ impl Symbolic {
                             self.memory[sym].value = Value::Array {
                                 len:    0,
                                 array:  HashMap::new(),
+                                null_initialized: false,
                             };
                         }
                     }
@@ -420,7 +423,7 @@ impl Symbolic {
                         )?;
                         self.memory[sym].value = Value::Integer(value);
 
-                        self.ssa.literal(sym, value, self.memory[sym].t.clone());
+                        self.ssa.literal((sym,0), value, self.memory[sym].t.clone());
 
                         value += 1;
                     }
@@ -804,12 +807,14 @@ impl Symbolic {
                             self.memory[sym].value = Value::Array {
                                 len:    val as usize,
                                 array:  HashMap::new(),
+                                null_initialized: false,
                             };
                             self.len_into_ssa(sym, expr.loc(), val as usize)?;
                         } else {
                             self.memory[sym].value = Value::Array {
                                 len:    0,
                                 array:  HashMap::new(),
+                                null_initialized: false,
                             };
                         }
                     }
@@ -819,7 +824,6 @@ impl Symbolic {
                     if let Some(assign) = assign {
                         let sym2 = self.execute_expr(assign)?;
                         self.copy(sym, sym2, loc)?;
-
                     };
                     if typed_o.t == ast::Type::Elided {
                         if self.memory[sym].typed.t == ast::Type::Elided {
@@ -872,6 +876,12 @@ impl Symbolic {
                             }
                             let sym = (sym, self.memory[sym].temporal);
 
+                            if let Value::Uninitialized = self.memory[sym.0].value {
+                                return Err(self.trace(format!("branch on uninitialized value"), vec![
+                                    (branch_expr.loc().clone(), format!("{} is uninitialized here", self.memory[sym.0].name))
+                                ]));
+                            }
+
 
                             self.ssa.bool_value(sym, |a,_model| match a {
                                 smt::Assertion::Constrained(val) => {
@@ -927,6 +937,11 @@ impl Symbolic {
                 ast::Statement::Return{loc, expr} => {
                     if let Some(expr) = expr  {
                         let e = self.execute_expr(expr)?;
+                        if let Value::Uninitialized = self.memory[e].value {
+                            return Err(self.trace(format!("return of uninitialized value"), vec![
+                                (expr.loc().clone(), format!("{} is uninitialized here", self.memory[e].name))
+                            ]));
+                        }
                         if let Some(retsym) =  self.current_function_ret {
                             self.copy(retsym, e, expr.loc())?;
                         }
@@ -1011,6 +1026,12 @@ impl Symbolic {
                     let lhs = self.execute_expr(lhs)?;
                     let rhs = self.execute_expr(rhs)?;
 
+                    if let Value::Uninitialized = self.memory[rhs].value {
+                        return Err(self.trace(format!("use of uninitialized rhs in assignment"), vec![
+                            (loc.clone(), format!("{} is uninitialized here", self.memory[rhs].name))
+                        ]));
+                    }
+
                     let (newtype, lhs, rhs) = self.type_coersion(lhs, rhs, loc)?;
 
 
@@ -1120,6 +1141,11 @@ impl Symbolic {
                             (expr.loc().clone(), format!("must be boolean"))
                         ]));
                     }
+                    if let Value::Uninitialized = self.memory[sym].value {
+                        return Err(self.trace(format!("branch on uninitialized value"), vec![
+                            (expr.loc().clone(), format!("{} is uninitialized here", self.memory[sym].name))
+                        ]));
+                    }
                     let sym = (sym, self.memory[sym].temporal);
                     self.cur().trace.push((sym.clone(), expr.loc().clone(),false));
 
@@ -1248,6 +1274,12 @@ impl Symbolic {
                     let mut calledarg = callargs.remove(0);
                     let mut callptr = self.execute_expr(&mut calledarg)?;
 
+                    if let Value::Uninitialized = self.memory[callptr].value {
+                        return Err(self.trace(format!("passing uninitialized value as argument"), vec![
+                            (calledarg.loc().clone(), format!("{} is uninitialized here", self.memory[callptr].name))
+                        ]));
+                    }
+
 
                     if self.memory[callptr].typed !=  defined[i].typed {
 
@@ -1353,7 +1385,118 @@ impl Symbolic {
     }
 
 
+    fn array_access(&mut self, lhs_sym: Symbol, rhs_sym: Symbol, loc: &ast::Location) -> Result<Symbol, Error> {
+        let static_index = if let smt::Assertion::Constrained(i)  = self.ssa.value((rhs_sym, self.memory[rhs_sym].temporal), |a,_|a) {
+            Some(i as usize)
+        } else {
+            None
+        };
+
+        let mut is_null_initialized = false;
+        match &self.memory[lhs_sym].value {
+            Value::Array{array, null_initialized, ..} => {
+                is_null_initialized = *null_initialized;
+                if let Some(i) = &static_index {
+                    if let Some(sym) = array.get(i) {
+                        return Ok(*sym);
+                    }
+                }
+            },
+            _ => ()
+        }
+
+        if self.memory[lhs_sym].t != smt::Type::Unsigned(64) {
+            return Err(self.trace(format!("cannot prove memory access due to unexpected type"), vec![
+                (loc.clone(), format!("lhs of array expression appears to be not a pointer or array"))
+            ]))
+        }
+
+        self.ssa.debug("begin array bounds");
+        let tmp1 = self.temporary(format!("len({})", self.memory[lhs_sym].name),
+        ast::Typed{
+            t:      ast::Type::USize,
+            ptr:    Vec::new(),
+            loc:    loc.clone(),
+            tail:   ast::Tail::None,
+        },
+        loc.clone(),
+        Tags::new(),
+        )?;
+        let lensym = self.builtin.get("len").expect("ICE: len theory not built in");
+        self.ssa.invocation(*lensym, vec![(lhs_sym, self.memory[lhs_sym].temporal)], (tmp1, 0));
+
+        let tmp2 = self.temporary(format!("{} < len({})", self.memory[rhs_sym].name, self.memory[lhs_sym].name),
+        ast::Typed{
+            t:      ast::Type::Bool,
+            ptr:    Vec::new(),
+            loc:    loc.clone(),
+            tail:   ast::Tail::None,
+        },
+        loc.clone(),
+        Tags::new(),
+        )?;
+
+        self.memory[tmp2].value = Value::InfixOp {
+            lhs:    (rhs_sym, self.memory[rhs_sym].temporal),
+            rhs:    (tmp1, 0),
+            op:     ast::InfixOperator::Lessthan,
+        };
+        self.ssa.infix_op(
+            tmp2,
+            (rhs_sym, self.memory[rhs_sym].temporal),
+            (tmp1, 0),
+            ast::InfixOperator::Lessthan,
+            smt::Type::Bool,
+            false,
+            );
+
+        self.ssa.debug("assert that length less than index is true");
+        self.ssa.assert(vec![(tmp2, self.memory[tmp2].temporal)], |a,model| match a {
+            false => {
+                let mut estack = Vec::new();
+                estack.extend(self.demonstrate(model.as_ref().unwrap(), (tmp2, self.memory[tmp2].temporal), 0));
+                Err(self.trace(format!("possible out of bounds array access"), estack))
+            }
+            true => {
+                Ok(())
+            }
+        })?;
+
+
+
+        let mut newtype = self.memory[lhs_sym].typed.clone();
+        newtype.ptr.pop();
+
+        let tmp = self.temporary(
+            format!("array member {}[{}]", self.memory[lhs_sym].name, self.memory[rhs_sym].name),
+            newtype,
+            loc.clone(),
+            self.memory[lhs_sym].tags.clone(),
+        )?;
+
+
+        if is_null_initialized {
+            self.memory[tmp].value = Value::Integer(0);
+            self.ssa.literal((tmp, 0), 0, self.memory[tmp].t.clone());
+        } else {
+            self.memory[tmp].value = Value::Unconstrained("array content".to_string());
+        }
+
+        match &mut self.memory[lhs_sym].value {
+            Value::Array{array, ..} => {
+                if let Some(i) = &static_index {
+                    array.insert(*i, tmp);
+                }
+            },
+            _ => ()
+        }
+
+        Ok(tmp)
+    }
+
+
 
+    //TODO much of thise code can be removed now because alloc() already initializes structs with members
     fn member_access(&mut self, lhs_sym: Symbol, rhs: &str, loc: &ast::Location) -> Result<Symbol, Error> {
 
         let mut struct_def = None;
@@ -1363,6 +1506,12 @@ impl Symbolic {
             }
         };
 
+        if let Value::Uninitialized = self.memory[lhs_sym].value {
+            return Err(self.trace(format!("member access of uninitialized value"), vec![
+                (loc.clone(), format!("{} is uninitialized here", self.memory[lhs_sym].name))
+            ]));
+        }
+
         let struct_def = match struct_def {
             Some(v) => v,
             None => {
@@ -1410,7 +1559,7 @@ impl Symbolic {
         }
 
 
-        let mut fieldvalue = Value::Uninitialized;
+        let mut fieldvalue = Value::Unconstrained("member access".to_string());
         let mut fieldtyped = field.1.typed.clone();
 
 
@@ -1433,6 +1582,7 @@ impl Symbolic {
                 fieldvalue = Value::Array {
                     len:    val as usize,
                     array:  HashMap::new(),
+                    null_initialized: false,
                 };
 
             // unsized array, but container has a tail
@@ -1440,6 +1590,7 @@ impl Symbolic {
                 fieldvalue = Value::Array {
                     len:    *val as usize,
                     array:  HashMap::new(),
+                    null_initialized: false,
                 };
             }
 
@@ -1582,102 +1733,7 @@ impl Symbolic {
                     ]))
                 }
 
-                let static_index = if let smt::Assertion::Constrained(i)  = self.ssa.value((rhs_sym, self.memory[rhs_sym].temporal), |a,_|a) {
-                    Some(i as usize)
-                } else {
-                    None
-                };
-                match &self.memory[lhs_sym].value {
-                    Value::Array{array, ..} => {
-                        if let Some(i) = &static_index {
-                            if let Some(sym) = array.get(i) {
-                                return Ok(*sym);
-                            }
-                        }
-                    },
-                    _ => ()
-                }
-
-                if self.memory[lhs_sym].t != smt::Type::Unsigned(64) {
-                    return Err(self.trace(format!("cannot prove memory access due to unexpected type"), vec![
-                        (lhs.loc().clone(), format!("lhs of array expression appears to be not a pointer or array"))
-                    ]))
-                }
-
-                self.ssa.debug("begin array bounds");
-                let tmp1 = self.temporary(format!("len({})", self.memory[lhs_sym].name),
-                ast::Typed{
-                    t:      ast::Type::USize,
-                    ptr:    Vec::new(),
-                    loc:    loc.clone(),
-                    tail:   ast::Tail::None,
-                },
-                loc.clone(),
-                Tags::new(),
-                )?;
-                let lensym = self.builtin.get("len").expect("ICE: len theory not built in");
-                self.ssa.invocation(*lensym, vec![(lhs_sym, self.memory[lhs_sym].temporal)], (tmp1, 0));
-
-                let tmp2 = self.temporary(format!("{} < len({})", self.memory[rhs_sym].name, self.memory[lhs_sym].name),
-                ast::Typed{
-                    t:      ast::Type::Bool,
-                    ptr:    Vec::new(),
-                    loc:    loc.clone(),
-                    tail:   ast::Tail::None,
-                },
-                loc.clone(),
-                Tags::new(),
-                )?;
-
-                self.memory[tmp2].value = Value::InfixOp {
-                    lhs:    (rhs_sym, self.memory[rhs_sym].temporal),
-                    rhs:    (tmp1, 0),
-                    op:     ast::InfixOperator::Lessthan,
-                };
-                self.ssa.infix_op(
-                    tmp2,
-                    (rhs_sym, self.memory[rhs_sym].temporal),
-                    (tmp1, 0),
-                    ast::InfixOperator::Lessthan,
-                    smt::Type::Bool,
-                    false,
-                    );
-
-                self.ssa.debug("assert that length less than index is true");
-                self.ssa.assert(vec![(tmp2, self.memory[tmp2].temporal)], |a,model| match a {
-                    false => {
-                        let mut estack = Vec::new();
-                        estack.extend(self.demonstrate(model.as_ref().unwrap(), (tmp2, self.memory[tmp2].temporal), 0));
-                        Err(self.trace(format!("possible out of bounds array access"), estack))
-                    }
-                    true => {
-                        Ok(())
-                    }
-                })?;
-
-
-
-                let mut newtype = self.memory[lhs_sym].typed.clone();
-                newtype.ptr.pop();
-
-                let tmp = self.temporary(
-                    format!("array member {}[{}]", self.memory[lhs_sym].name, self.memory[rhs_sym].name),
-                    newtype,
-                    loc.clone(),
-                    self.memory[lhs_sym].tags.clone(),
-                )?;
-                self.memory[tmp].value = Value::Unconstrained("array content".to_string());
-
-                match &mut self.memory[lhs_sym].value {
-                    Value::Array{array, ..} => {
-                        if let Some(i) = &static_index {
-                            array.insert(*i, tmp);
-                        }
-                    },
-                    _ => ()
-                }
-
-                Ok(tmp)
+                self.array_access(lhs_sym, rhs_sym, loc)
             },
             ast::Expression::LiteralString{ loc, v } => {
                 let tmp = self.temporary(
@@ -1697,6 +1753,7 @@ impl Symbolic {
                 self.memory[tmp].value = Value::Array{
                     array:  HashMap::new(),
                     len:    v.len(),
+                    null_initialized: false,
                 };
                 self.ssa_mark_safe(tmp, loc)?;
                 self.ssa_mark_nullterm(tmp, loc)?;
@@ -2235,6 +2292,17 @@ impl Symbolic {
                 let lhs_sym = self.execute_expr(lhs)?;
                 let rhs_sym = self.execute_expr(rhs)?;
 
+                if let Value::Uninitialized = self.memory[lhs_sym].value {
+                    return Err(self.trace(format!("use of uninitialized value"), vec![
+                        (lhs.loc().clone(), format!("{} is uninitialized here", self.memory[lhs_sym].name))
+                    ]));
+                }
+                if let Value::Uninitialized = self.memory[rhs_sym].value {
+                    return Err(self.trace(format!("use of uninitialized value"), vec![
+                        (rhs.loc().clone(), format!("{} is uninitialized here", self.memory[rhs_sym].name))
+                    ]));
+                }
+
                 let (mut newtype, lhs_sym, rhs_sym) = self.type_coersion(lhs_sym, rhs_sym, loc)?;
 
                 if !op.takes_boolean() && newtype.t == ast::Type::Bool{
@@ -2378,7 +2446,7 @@ impl Symbolic {
                         if let Some(nuval) = self.ssa.value((len_of_opresult, self.memory[len_of_opresult].temporal), |a,_|match a{
                             smt::Assertion::Constrained(val) => {
                                 let nuarray = HashMap::new();
-                                Some(Value::Array{len: val as usize, array: nuarray})
+                                Some(Value::Array{len: val as usize, array: nuarray, null_initialized: false})
                             }
                             _ => None,
                         }) {
@@ -2489,7 +2557,7 @@ impl Symbolic {
                         // it must be coming from a virtual stack
                         // because if we want to prove pointer arithmetic
                         // this value is meaningless
-                        self.ssa.literal(tmp, lhs_sym as u64, smt::Type::Unsigned(64));
+                        self.ssa.literal((tmp, 0), lhs_sym as u64, smt::Type::Unsigned(64));
 
                         self.ssa_mark_safe(tmp, loc)?;
                         Ok(tmp)
@@ -2611,6 +2679,7 @@ impl Symbolic {
                 self.memory[aptr].value = Value::Array{
                     len:    array.len(),
                     array,
+                    null_initialized: false,
                 };
                 self.ssa_mark_safe(aptr, loc)?;
 
@@ -2653,6 +2722,15 @@ impl Symbolic {
         if let Value::Address(to) = self.memory[lhs_sym].value.clone() {
             return Ok(to);
         }
+        if let Value::Array{..} = self.memory[lhs_sym].value {
+            let mut expr = ast::Expression::Literal{
+                loc: loc.clone(),
+                v:   "0".to_string(),
+            };
+            let rhs_sym = self.execute_expr(&mut expr)?;
+            return self.array_access(lhs_sym, rhs_sym, loc);
+        }
+
 
         let mut nutype = self.memory[lhs_sym].typed.clone();
         let popped_tags = match nutype.ptr.pop() {
@@ -2670,7 +2748,6 @@ impl Symbolic {
             popped_tags,
         )?;
 
-
         if self.memory[lhs_sym].t != smt::Type::Unsigned(64) {
             return Err(self.trace(format!("cannot prove memory access due to unexpected type"), vec![
                 (loc.clone(), format!("deref expression appears to be not a pointer or array"))
@@ -2678,9 +2755,10 @@ impl Symbolic {
         }
 
 
-        // this is because the optimization cheat in check check_function_model doesn't apply
+        // skip safety check because the optimization cheat in check check_function_model doesn't apply
         // anything in between model calls
         if self.in_model {
+            self.memory[lhs_sym].value = Value::Address(member);
             return Ok(member);
         }
 
@@ -2714,7 +2792,7 @@ impl Symbolic {
 
 
         match &self.memory[lhs_sym].value {
-            // we're assuming this is ok because odf the above satefy checks
+            // we're assuming this is ok because of the above satefy checks
             Value::Uninitialized | Value::Unconstrained(_) => {
                 self.memory[lhs_sym].value = Value::Address(member);
             },
@@ -2765,6 +2843,100 @@ impl Symbolic {
         }
     }
 
+
+    fn typed_alloc(&mut self, sym: Symbol, typed: &ast::Typed, loc: &ast::Location, initialized: bool) -> Result<() , Error> {
+        if typed.ptr.len() > 0 {
+            return Ok(());
+        }
+        if let ast::Type::Other(name) = &typed.t {
+            if let Some(def) = self.defs.get(name) {
+                let def = def.clone();
+                if let ast::Def::Struct{fields, ..} = def {
+                    let mut members = HashMap::new();
+                    for field in fields {
+
+                        let mut fieldvalue = Value::Uninitialized;
+                        if initialized {
+                            fieldvalue = Value::Unconstrained("member".to_string());
+                        }
+                        let mut fieldtyped = field.typed.clone();
+
+                        if let Some(array) = &field.array {
+
+                            // sized array
+                            if let Some(expr) = array {
+                                let mut expr = expr.clone();
+                                let asym = self.execute_expr(&mut expr)?;
+                                let val = self.ssa.value((asym, self.memory[asym].temporal), |a,_| match a {
+                                    smt::Assertion::Constrained(i) => {
+                                        Ok(i)
+                                    },
+                                    _ => {
+                                        Err(self.trace("array size must be static".to_string(), vec![
+                                                       (expr.loc().clone(), format!("expression cannot be reduced to a constrained value at compile time"))
+                                        ]))
+                                    }
+                                })?;
+                                fieldvalue = Value::Array {
+                                    len:    val as usize,
+                                    array:  HashMap::new(),
+                                    null_initialized: false,
+                                };
+
+                                // unsized array, but container has a tail
+                            } else if let ast::Tail::Static(val,_loc) = &self.memory[sym].typed.tail {
+                                fieldvalue = Value::Array {
+                                    len:    *val as usize,
+                                    array:  HashMap::new(),
+                                    null_initialized: false,
+                                };
+                            }
+
+                            fieldtyped.ptr.push(ast::Pointer{
+                                loc:  field.loc.clone(),
+                                tags: Tags::new(),
+                            });
+                        }
+
+                        //nested tail
+                        match field.typed.tail {
+                            ast::Tail::Dynamic => {
+                                fieldtyped.tail = self.memory[sym].typed.tail.clone();
+                            }
+                            _ => {},
+                        }
+
+                        let tmp = self.temporary(
+                            format!("{}.{}", self.memory[sym].name, field.name),
+                            fieldtyped.clone(),
+                            loc.clone(),
+                            field.tags.clone(),
+                        )?;
+
+
+                        match (&fieldvalue, &field.array) {
+                            (Value::Array{len,..}, _) if *len > 0 => {
+                                self.len_into_ssa(tmp, loc, *len)?;
+                                self.ssa_mark_safe(tmp, loc)?;
+                            },
+                            (_, Some(_)) => {
+                                // access to an array member as pointer is always safe, because its part of the struct mem
+                                self.ssa_mark_safe(tmp, loc)?;
+                            },
+                            _ => (),
+                        }
+                        self.memory[tmp].value = fieldvalue;
+                        self.typed_alloc(tmp, &fieldtyped, loc, initialized)?;
+                        members.insert(field.name.clone(), tmp);
+
+                    }
+                    self.memory[sym].value = Value::Struct{members};
+                }
+            }
+        }
+        return Ok(());
+    }
+
     // new stack variable
     fn alloc(&mut self, name: Name, typed: ast::Typed, loc: ast::Location, tags: ast::Tags) -> Result<Symbol, Error> {
         self.ssa.debug_loc(&loc);
@@ -2793,13 +2965,7 @@ impl Symbolic {
         self.cur().locals.insert(name.clone(), symbol);
         self.ssa.declare(symbol, &format!("{}", name), t);
 
-
-        if let ast::Type::Other(name) = &typed.t {
-            if let Some(def) = self.defs.get(name) {
-                if let ast::Def::Struct{..} = def {
-                }
-            }
-        }
+        self.typed_alloc(symbol, &typed, &loc, false)?;
 
 
 
@@ -2885,7 +3051,7 @@ impl Symbolic {
             typed:      typed.clone(),
             name:       Name::from(&name),
             declared:   loc.clone(),
-            value:      Value::Uninitialized,
+            value:      Value::Unconstrained("temp".to_string()),
             tags,
             temporal:   0,
             assignments: HashMap::new(),
@@ -2893,9 +3059,51 @@ impl Symbolic {
         });
         debug!("{} {} := {}", name, typed, symbol);
         self.ssa.declare(symbol, &format!("{}", name), t);
+        self.typed_alloc(symbol, &typed, &loc, true)?;
         Ok(symbol)
     }
 
+    fn make_all_null(&mut self, lhs: Symbol, loc: &ast::Location) -> Result<(), Error> {
+        match self.memory[lhs].typed.t {
+            ast::Type::Other(_) => {
+                self.typed_alloc(lhs, &self.memory[lhs].typed.clone(), loc, true)?;
+                match &mut self.memory[lhs].value {
+                    Value::Void             => (),
+                    Value::Uninitialized    => {
+                    },
+                    Value::Integer(ref mut s)       => {
+                        *s = 0;
+                    }
+                    Value::InfixOp{..}      => (),
+                    Value::PrefixOp{..}     => (),
+                    Value::PostfixOp{..}    => (),
+                    Value::Struct{ref members}   => {
+                        for (mn,member) in members.clone() {
+                            self.make_all_null(member, loc)?;
+                        }
+                    }
+                    Value::Array{len,array, null_initialized} => {
+                        *null_initialized = true;
+                        for (_, m) in array.clone() {
+                            self.make_all_null(m, loc)?;
+                        }
+                    },
+                    Value::Address(_)       => {
+                    },
+                    Value::Unconstrained(s) => {
+                    },
+                    Value::Theory{..}       => (),
+                    Value::Function{..}     => (),
+                    Value::SelfCall{..}     => (),
+                }
+            }
+            _ => {
+                self.memory[lhs].value = Value::Integer(0);
+                self.ssa.literal((lhs, self.memory[lhs].temporal), 0, self.memory[lhs].t.clone());
+            }
+        }
+        Ok(())
+    }
 
     //                  cpy here   from here
     fn copy(&mut self, lhs: Symbol, rhs: Symbol, used_here: &ast::Location) -> Result<(), Error> {
@@ -2939,7 +3147,6 @@ impl Symbolic {
         self.memory[lhs].assignments.insert(tt, used_here.clone());
 
 
-
         match self.memory[rhs].value.clone() {
             Value::Void => {
                 return Err(self.trace(format!("void is not a value: '{}'",  self.memory[rhs].name), vec![
@@ -2947,10 +3154,10 @@ impl Symbolic {
                 ]));
             }
             Value::Uninitialized => {
-                // FIXME for now this is too noisy.
-                //return Err(self.trace(format!("unsafe read access to uninitialized local '{}'", self.memory[rhs].name), vec![
-                //    (used_here.clone(), "used here".to_string())
-                //]));
+                // TODO for now this is too noisy.
+                return Err(self.trace(format!("unsafe read access to uninitialized local '{}'", self.memory[rhs].name), vec![
+                    (used_here.clone(), "used here".to_string())
+                ]));
             }
             Value::Theory{..} => {
                 return Err(self.trace(format!("taking the value of a theory is not a thing"), vec![
@@ -2992,7 +3199,24 @@ impl Symbolic {
 
                        self.len_into_ssa(lhs, used_here, prev.len())?;
                    }
+                   Value::Struct{..} => {
+                       if len != 1 {
+                           return Err(self.trace(format!("assigning arrays to struct"), vec![
+                                (used_here.clone(), format!("can only use {{0}} here"))
+                           ]));
+                       }
+
+                       if let Value::Integer(0) = self.memory[array[&0]].value {
+                       } else {
+                           return Err(self.trace(format!("assigning arrays to struct"), vec![
+                                (used_here.clone(), format!("can only use {{0}} here"))
+                           ]));
+                       }
+
+                       return self.make_all_null(lhs, used_here);
+                   }
                    _ => {
+                       value = self.memory[rhs].value.clone();
                        self.len_into_ssa(lhs, used_here, len)?;
                    }
                }
@@ -3063,7 +3287,7 @@ impl Symbolic {
         )?;
         let thsym = self.builtin.get("safe").expect("ICE: safe theory not built in");
         self.ssa.invocation(*thsym, vec![(sym, self.memory[sym].temporal)], (tmp, 0));
-        self.ssa.literal(tmp, 1, smt::Type::Bool);
+        self.ssa.literal((tmp, 0), 1, smt::Type::Bool);
         Ok(())
     }
 
@@ -3084,7 +3308,7 @@ impl Symbolic {
         )?;
         let thsym = self.builtin.get("nullterm").expect("ICE: nullterm theory not built in");
         self.ssa.invocation(*thsym, vec![(sym, self.memory[sym].temporal)], (tmp,0));
-        self.ssa.literal(tmp, 1, smt::Type::Bool);
+        self.ssa.literal((tmp, 0), 1, smt::Type::Bool);
         Ok(())
     }
 
@@ -3102,7 +3326,7 @@ impl Symbolic {
         )?;
         let lensym = self.builtin.get("len").expect("ICE: len theory not built in");
         self.ssa.invocation(*lensym, vec![(sym, self.memory[sym].temporal)], (tmp, 0));
-        self.ssa.literal(tmp, len as u64, smt::Type::Unsigned(64));
+        self.ssa.literal((tmp, 0), len as u64, smt::Type::Unsigned(64));
         Ok(())
     }
 
@@ -3193,7 +3417,7 @@ impl Symbolic {
                     Tags::new(),
                 )?;
                 self.memory[sym].value = value;
-                self.ssa.literal(sym, v as u64, self.memory[sym].t.clone());
+                self.ssa.literal((sym, 0), v as u64, self.memory[sym].t.clone());
                 self.ssa_mark_valid(sym, loc)?;
                 Ok(sym)
             },
diff --git a/tests/mustpass/borrow_attestation/.gitignore b/tests/mustfail/uninitialized_branch/.gitignore
similarity index 100%
rename from tests/mustpass/borrow_attestation/.gitignore
rename to tests/mustfail/uninitialized_branch/.gitignore
diff --git "a/tests/mustfail/uninitialized_branch/\\" "b/tests/mustfail/uninitialized_branch/\\"
new file mode 100644
index 0000000..5cd6845
--- /dev/null
+++ "b/tests/mustfail/uninitialized_branch/\\"
@@ -0,0 +1,15 @@
+using <stdio.h>::{printf};
+
+export fn main() -> int {
+
+    bool ok;
+
+
+    if false && ok{
+        return ok;
+    }
+
+
+    printf("hello uninitialized_branch\n");
+    return 0;
+}
diff --git a/tests/mustfail/uninitialized_branch/src/main.zz b/tests/mustfail/uninitialized_branch/src/main.zz
new file mode 100644
index 0000000..5cd6845
--- /dev/null
+++ b/tests/mustfail/uninitialized_branch/src/main.zz
@@ -0,0 +1,15 @@
+using <stdio.h>::{printf};
+
+export fn main() -> int {
+
+    bool ok;
+
+
+    if false && ok{
+        return ok;
+    }
+
+
+    printf("hello uninitialized_branch\n");
+    return 0;
+}
diff --git a/tests/mustfail/uninitialized_branch/zz.toml b/tests/mustfail/uninitialized_branch/zz.toml
new file mode 100644
index 0000000..d9bb2d6
--- /dev/null
+++ b/tests/mustfail/uninitialized_branch/zz.toml
@@ -0,0 +1,13 @@
+[project]
+version = "0.1.0"
+name = "uninitialized_branch"
+cincludes = []
+cobjects = []
+pkgconfig = []
+cflags = []
+lflags = []
+
+[variants]
+default = []
+
+[dependencies]
diff --git a/tests/mustpass/arith_arith/src/main.zz b/tests/mustpass/arith_arith/src/main.zz
index 9636a1d..b31129e 100644
--- a/tests/mustpass/arith_arith/src/main.zz
+++ b/tests/mustpass/arith_arith/src/main.zz
@@ -11,6 +11,7 @@ export fn main() -> int {
 
     int y = *b;
 
+    static_assert(len(b) > 10 );
     int *c = b + 10;
     static_assert(len(c) == 90);
 
diff --git a/tests/mustpass/borrow_attestation/src/main.zz b/tests/mustpass/borrow_attestation/src/main.zz
deleted file mode 100644
index ffbaae8..0000000
--- a/tests/mustpass/borrow_attestation/src/main.zz
+++ /dev/null
@@ -1,38 +0,0 @@
-using <stdio.h>::{printf};
-
-
-struct Always1 {
-    int a;
-}
-
-fn borrow(Always1 * self) -> Always1 *
-    where safe(self)
-    where self->a == 1
-    model safe(return)
-    model return->a == 1
-{
-    return self;
-}
-
-
-fn new(Always1 mut uninitialized * self)
-    model self->a == 1
-{
-    self->a = 1;
-}
-
-
-fn something(Always1 *self)
-{
-    static_assert(self->a == 1);
-}
-
-export fn main() -> int {
-
-    Always1 mut a = {0};
-    a.new();
-    a.something();
-
-    printf("hello integrity\n");
-    return 0;
-}
diff --git a/tests/mustpass/branch_dont_loose_deref/src/main.zz b/tests/mustpass/branch_dont_loose_deref/src/main.zz
index 0dc1420..923eaeb 100644
--- a/tests/mustpass/branch_dont_loose_deref/src/main.zz
+++ b/tests/mustpass/branch_dont_loose_deref/src/main.zz
@@ -15,8 +15,8 @@ pub fn parse_query(Store mut*store, usize answers) -> bool
 {
     usize mut storepos = 0;
 
-    bool mut it;
-    while it  {
+    bool mut it = true;
+    if it  {
         /// the bug was that we did a deref here
         ((store->broker)[storepos]).protocol = 2;
     }
diff --git a/tests/mustpass/branch_effect/src/main.zz b/tests/mustpass/branch_effect/src/main.zz
index 6c86016..536bc5a 100644
--- a/tests/mustpass/branch_effect/src/main.zz
+++ b/tests/mustpass/branch_effect/src/main.zz
@@ -1,7 +1,7 @@
 using <stdio.h>::{printf};
 
 export fn main() -> int {
-    int x;
+    int x = 23;
 
     if x != 2 {
         return 0;
diff --git a/tests/mustpass/branch_effect2/src/main.zz b/tests/mustpass/branch_effect2/src/main.zz
index fc97bcf..11cf15f 100644
--- a/tests/mustpass/branch_effect2/src/main.zz
+++ b/tests/mustpass/branch_effect2/src/main.zz
@@ -28,7 +28,7 @@ export fn main() -> int {
     boh(&e);
 
 
-    int x;
+    int x = 911;
     if x != 2 {
         return 0;
     }
diff --git a/tests/mustpass/fn_vtable_ctor/src/main.zz b/tests/mustpass/fn_vtable_ctor/src/main.zz
index 5b7e120..77246b4 100644
--- a/tests/mustpass/fn_vtable_ctor/src/main.zz
+++ b/tests/mustpass/fn_vtable_ctor/src/main.zz
@@ -26,7 +26,7 @@ export fn main() -> int {
     };
     int x = mm.add(1,8);
 
-    Math mut m;
+    Math mut m = {0};
     new(&m, add_impl);
 
     int x2 = m.add(1,8);
diff --git a/tests/mustpass/loop_condition/src/main.zz b/tests/mustpass/loop_condition/src/main.zz
index 29259df..ab99b1a 100644
--- a/tests/mustpass/loop_condition/src/main.zz
+++ b/tests/mustpass/loop_condition/src/main.zz
@@ -4,6 +4,11 @@ using <stdio.h>::{printf};
 
 inline fn alias(void * alias a) {}
 
+
+fn rand() -> int {
+    return 42;
+}
+
 export fn main() -> int {
 
 
@@ -39,12 +44,12 @@ export fn main() -> int {
         }
 
 
-        int uninitialized;
+        int something = rand();
 
-        if uninitialized == 2 {
+        if something == 2 {
             continue;
         }
-        static_assert(uninitialized != 2);
+        static_assert(something != 2);
 
 
         // this is a workaround until symbolic understands loop passes
diff --git a/tests/mustpass/nullstruct/.gitignore b/tests/mustpass/nullstruct/.gitignore
new file mode 100644
index 0000000..90431dd
--- /dev/null
+++ b/tests/mustpass/nullstruct/.gitignore
@@ -0,0 +1,3 @@
+/target
+.gdb_history
+vgcore.*
diff --git a/tests/mustpass/nullstruct/src/main.zz b/tests/mustpass/nullstruct/src/main.zz
new file mode 100644
index 0000000..cb1a329
--- /dev/null
+++ b/tests/mustpass/nullstruct/src/main.zz
@@ -0,0 +1,12 @@
+using <stdio.h>::{printf};
+
+
+struct A {
+    int a;
+}
+
+export fn main() -> int {
+    A a = {0};
+    static_assert(a.a == 0);
+    return 0;
+}
diff --git a/tests/mustpass/borrow_attestation/zz.toml b/tests/mustpass/nullstruct/zz.toml
similarity index 83%
rename from tests/mustpass/borrow_attestation/zz.toml
rename to tests/mustpass/nullstruct/zz.toml
index 4c59337..d6a9074 100644
--- a/tests/mustpass/borrow_attestation/zz.toml
+++ b/tests/mustpass/nullstruct/zz.toml
@@ -1,6 +1,6 @@
 [project]
 version = "0.1.0"
-name = "borrow_attestation"
+name = "nullstruct"
 cincludes = []
 cobjects = []
 pkgconfig = []
diff --git a/tests/mustpass/smt_commutative/src/main.zz b/tests/mustpass/smt_commutative/src/main.zz
index 5e9b978..f0e8aeb 100644
--- a/tests/mustpass/smt_commutative/src/main.zz
+++ b/tests/mustpass/smt_commutative/src/main.zz
@@ -3,6 +3,11 @@ using <stdio.h>::{printf};
 
 
 
+fn rand() -> usize {
+    return 42;
+}
+
+
 export fn bob(int * unsafe i, usize y)
     where len(i) >= y
 {
@@ -13,8 +18,8 @@ export fn bob(int * unsafe i, usize y)
 export fn main() -> int {
 
 
-    int     *i;
-    usize   y;
+    int     *i = rand();
+    usize   y = rand();
     static_attest(y <= len(i));
 
     bob(i, y);
diff --git a/tests/mustpass/static_attest_in_third_branch/src/main.zz b/tests/mustpass/static_attest_in_third_branch/src/main.zz
index 199162d..4fff195 100644
--- a/tests/mustpass/static_attest_in_third_branch/src/main.zz
+++ b/tests/mustpass/static_attest_in_third_branch/src/main.zz
@@ -6,6 +6,10 @@ fn doh(int *a)
     
 }
 
+fn rand() -> bool {
+    return true;
+}
+
 fn from_str(bool whatever, int * i)
     where bob(*i)
 {
@@ -20,7 +24,7 @@ fn from_str(bool whatever, int * i)
 
     static_attest(bob(*i));
 
-    bool somethingelse;
+    bool somethingelse = rand();
 
     if (somethingelse) {
         doh(i);
diff --git a/tests/mustpass/structs/src/main.zz b/tests/mustpass/structs/src/main.zz
index c7fd7de..50981e1 100644
--- a/tests/mustpass/structs/src/main.zz
+++ b/tests/mustpass/structs/src/main.zz
@@ -53,7 +53,7 @@ export fn main() -> int {
 
 
 
-    V mut v;
+    V mut v = {0};
     (v.a).a = 1;
 
     peter(&v);
diff --git a/tests/mustpass/syntax_accesspreceeedence/src/main.zz b/tests/mustpass/syntax_accesspreceeedence/src/main.zz
index 69cb860..bb8190c 100644
--- a/tests/mustpass/syntax_accesspreceeedence/src/main.zz
+++ b/tests/mustpass/syntax_accesspreceeedence/src/main.zz
@@ -13,7 +13,7 @@ struct B {
 
 export fn main() -> int {
 
-    B mut b;
+    B mut b = {0};
     b.a.a= 3;
 
 
diff --git a/zz.vim/syntax/zz.vim b/zz.vim/syntax/zz.vim
index 505d45c..239abd3 100644
--- a/zz.vim/syntax/zz.vim
+++ b/zz.vim/syntax/zz.vim
@@ -16,6 +16,7 @@ syn keyword zzImport            using
 syn keyword zzVisibility        export pub
 syn keyword zzKeywords          mut as
 syn keyword zzSelf              self
+syn keyword zzSpecial           new
 syn keyword zzDanger            unsafe
 syn keyword zzOperator          len safe static_attest static_assert nullterm
 syn keyword zzSSA1              where
@@ -38,6 +39,7 @@ hi def link zzSSA1              Structure
 hi def link zzSSA2              cString
 hi def link zzString            cString
 hi def link zzSelf              Constant
+hi def link zzSpecial           Structure
 
 let b:current_syntax = "zz"