diff --git a/src/CGContext.cpp b/src/CGContext.cpp
index 0c70740ad..6a7110431 100644
--- a/src/CGContext.cpp
+++ b/src/CGContext.cpp
@@ -202,13 +202,13 @@ CGContext::read_var(const Variable *v)
 bool
 CGContext::check_read_var(const Variable *v, const std::vector<const Fact*>& facts)
 {
-	if (v->is_union_field() && FactUnion::is_nonreadable_field(v, facts)) {
+	if (!read_indices(v, facts)) {
 		return false;
 	}
-	if (!read_indices(v, facts)) {
+	v = v->get_collective();	
+	if (FactUnion::is_nonreadable_field(v, facts)) {
 		return false;
 	}
-	v = v->get_collective();
 	if (is_nonreadable(v)) {
 		return false;
 	} 
diff --git a/src/Constant.cpp b/src/Constant.cpp
index d0489945b..c64e02e89 100644
--- a/src/Constant.cpp
+++ b/src/Constant.cpp
@@ -433,6 +433,17 @@ Constant::equals(int num) const
 	return StringUtils::str2int(value) == num;
 }
 
+string
+Constant::get_field(size_t fid) const
+{
+	vector<string> fields;
+	StringUtils::split_string(value, fields, "{},");
+	if (fid < fields.size()) {
+		return fields[fid];
+	}
+	return "";
+}
+
 ///////////////////////////////////////////////////////////////////////////////
 
 /*
diff --git a/src/Constant.h b/src/Constant.h
index 4c268aea1..c59c15c4c 100644
--- a/src/Constant.h
+++ b/src/Constant.h
@@ -73,6 +73,8 @@ class Constant : public Expression
 	// Unused:
 	const std::string &get_value(void) const { return value; }
 	
+	string get_field(size_t fid) const;
+
 	virtual bool less_than(int num) const;
 	virtual bool not_equals(int num) const;
 	virtual bool equals(int num) const;
diff --git a/src/DefaultRndNumGenerator.cpp b/src/DefaultRndNumGenerator.cpp
index ca0949de0..074e35d38 100644
--- a/src/DefaultRndNumGenerator.cpp
+++ b/src/DefaultRndNumGenerator.cpp
@@ -33,6 +33,7 @@
 #include <cstdlib>
 #include <iostream>
 #include <sstream>
+#include <fstream>
 
 #include "Filter.h"
 #include "SequenceFactory.h"
@@ -116,9 +117,15 @@ DefaultRndNumGenerator::add_number(int v, int bound, int k)
 unsigned int
 DefaultRndNumGenerator::rnd_upto(const unsigned int n, const Filter *f, const std::string *where)
 {
+	static int g = 0;
+	int h = g;
+	if (h == 440)
+		BREAK_NOP;   // for debugging
 	unsigned int v = genrand() % n;
 	unsigned INT64 local_depth = rand_depth_;
 	rand_depth_++;
+	//ofstream out("rnd.log", ios_base::app);
+	//out << g++ << ": " << v << "(" << n << ")" << endl;
 
 	if (f) {
 		while (f->filter(v)) {
@@ -127,8 +134,10 @@ DefaultRndNumGenerator::rnd_upto(const unsigned int n, const Filter *f, const st
 			// This will also overwrite the value added in the map.
 			rand_depth_ = local_depth+1;
 			v = genrand() % n;
+			/*out << g++ << ": " << v << "(" << n << ")" << endl;*/
 		}
 	}
+	//out.close();
 	if (where) {
 	std::ostringstream ss;
 		ss << *where << "->";
diff --git a/src/Effect.cpp b/src/Effect.cpp
index ec5131630..eb49a3821 100644
--- a/src/Effect.cpp
+++ b/src/Effect.cpp
@@ -440,37 +440,39 @@ Effect::field_is_written(const Variable *v) const
 bool
 Effect::sibling_union_field_is_read(const Variable *v) const
 {   
-	while (v->field_var_of) {
-		// check other fields of the union
-		if (v->field_var_of->type->eType == eUnion) {
-			for (size_t j=0; j<v->field_var_of->field_vars.size(); j++) {
-				Variable* field_var = v->field_var_of->field_vars[j];
-				if (field_var == v) continue;
-				if (is_read(field_var) || field_is_read(field_var)) {
-					return true; 
-				}
+	const Variable* you = v->get_collective();
+	// find the union variable(s) that contains you
+	for (; you && you->type->eType != eUnion; you = you->field_var_of)
+		;
+	if (you) {
+		for (size_t i=0; i<read_vars.size(); i++) {
+			const Variable* me = read_vars[i]->get_collective(); 
+			for (; me && me->type->eType != eUnion; me = me->field_var_of)
+				;
+			if (you == me) {
+				return true;
 			}
 		}
-		v = v->field_var_of;
 	}
 	return false;
 }
 
 bool
 Effect::sibling_union_field_is_written(const Variable *v) const
-{   
-	while (v->field_var_of) {
-		// check other fields of the union
-		if (v->field_var_of->type->eType == eUnion) {
-			for (size_t j=0; j<v->field_var_of->field_vars.size(); j++) {
-				Variable* field_var = v->field_var_of->field_vars[j];
-				if (field_var == v) continue;
-				if (is_written(field_var) || field_is_written(field_var)) {
-					return true; 
-				}
+{    
+	const Variable* you = v->get_collective();
+	// find the union variable(s) that contains you
+	for (; you && you->type->eType != eUnion; you = you->field_var_of)
+		;
+	if (you) {
+		for (size_t i=0; i<write_vars.size(); i++) {
+			const Variable* me = write_vars[i]->get_collective(); 
+			for (; me && me->type->eType != eUnion; me = me->field_var_of)
+				;
+			if (you == me) {
+				return true;
 			}
 		}
-		v = v->field_var_of;
 	}
 	return false;
 }
@@ -621,7 +623,7 @@ bool
 Effect::union_field_is_read(void) const
 { 
 	for (size_t i=0; i<read_vars.size(); i++) {
-		if (read_vars[i]->is_union_field()) {
+		if (read_vars[i]->is_inside_union_field()) {
 			return true;
 		}
 	}
diff --git a/src/Expression.cpp b/src/Expression.cpp
index 337282a77..1abd4fea0 100644
--- a/src/Expression.cpp
+++ b/src/Expression.cpp
@@ -40,7 +40,6 @@
 #include <cassert>
 
 #include "Common.h"
-
 #include "CGContext.h"
 #include "CGOptions.h"
 #include "Effect.h"
@@ -50,7 +49,8 @@
 #include "Constant.h" // temporary; don't want to depend on subclass!
 #include "ExpressionFuncall.h" // temporary; don't want to depend on subclass!
 #include "ExpressionVariable.h" // temporary; don't want to depend on subclass!
-
+#include "ExpressionAssign.h"
+#include "ExpressionComma.h"
 #include "Error.h"
 #include "ProbabilityTable.h"
 #include "PartialExpander.h"
@@ -60,28 +60,7 @@
 
 int eid = 0;
 
-class ExpressionFilter : public Filter {
-public:
-	ExpressionFilter();
-
-	virtual ~ExpressionFilter();
-
-	virtual bool filter(int v) const = 0;
-
-	eTermType number_to_termtype(unsigned int v, ProbabilityTable<unsigned int, eTermType> *table) const;
-};
-
-ExpressionFilter::ExpressionFilter()
-{
-
-}
-
-ExpressionFilter::~ExpressionFilter()
-{
-
-}
-
-ProbabilityTable<unsigned int, eTermType> *Expression::exprTable_ = NULL;
+ProbabilityTable<unsigned int, int> *Expression::exprTable_ = NULL;
 
 void
 Expression::InitExprProbabilityTable()
@@ -89,23 +68,27 @@ Expression::InitExprProbabilityTable()
 	if (Expression::exprTable_)
 		return;
 
-	Expression::exprTable_ = new ProbabilityTable<unsigned int, eTermType>();
-	Expression::exprTable_->add_elem(60, eFunction);
-	Expression::exprTable_->add_elem(70, eConstant);
-	Expression::exprTable_->add_elem(100, eVariable);
+	Expression::exprTable_ = new ProbabilityTable<unsigned int, int>();
+	Expression::exprTable_->add_elem(40, (int)eFunction);
+	Expression::exprTable_->add_elem(50, (int)eAssignment);
+	Expression::exprTable_->add_elem(60, (int)eCommaExpr);
+	Expression::exprTable_->add_elem(70, (int)eConstant);
+	Expression::exprTable_->add_elem(100, (int)eVariable);
 }
 
-ProbabilityTable<unsigned int, eTermType> *Expression::paramTable_ = NULL;
+ProbabilityTable<unsigned int, int> *Expression::paramTable_ = NULL;
 void
 Expression::InitParamProbabilityTable()
 {
 	if (Expression::paramTable_)
 		return;
 
-	Expression::paramTable_ = new ProbabilityTable<unsigned int, eTermType>();
-	Expression::paramTable_->add_elem(30, eFunction);
-	Expression::paramTable_->add_elem(40, eConstant);
-	Expression::paramTable_->add_elem(100, eVariable);
+	Expression::paramTable_ = new ProbabilityTable<unsigned int, int>();
+	Expression::paramTable_->add_elem(30, (int)eFunction);
+	Expression::paramTable_->add_elem(40, (int)eConstant);
+	Expression::paramTable_->add_elem(50, (int)eAssignment);
+	Expression::paramTable_->add_elem(60, (int)eCommaExpr);
+	Expression::paramTable_->add_elem(100, (int)eVariable);
 }
 
 void
@@ -115,105 +98,13 @@ Expression::InitProbabilityTables()
 	Expression::InitParamProbabilityTable();
 }
 
-eTermType
-ExpressionFilter::number_to_termtype(unsigned int i, ProbabilityTable<unsigned int, eTermType> *table) const
-{
-	assert(table);
-	return table->get_value(i);
-}
-
-/////////////////////////////////////////////////////////
-class DefaultExpressionFilter : public ExpressionFilter {
-public:
-	DefaultExpressionFilter(const Type &type, bool no_func, bool no_const);
-
-	virtual ~DefaultExpressionFilter();
-
-	virtual bool filter(int v) const;
-
-private:
-	const Type &type_;
-
-	const bool no_func_;
-	const bool no_const_;
-};
-
-
-DefaultExpressionFilter::DefaultExpressionFilter(const Type &type, bool no_func, bool no_const)
-	: type_(type),
-	  no_func_(no_func),
-	  no_const_(no_const)
-{
-
-}
-
-DefaultExpressionFilter::~DefaultExpressionFilter()
-{
-
-}
-
-bool
-DefaultExpressionFilter::filter(int v) const
-{
-	if (!this->valid_filter())
-		return false;
-
-	if (Expression::exprTable_->filter(v))
-		return true;
-
-	eTermType tt = number_to_termtype(v, Expression::exprTable_);
-	if (!CGOptions::return_structs() && tt == eFunction && type_.eType == eStruct)
-		return true;
-	if (!CGOptions::return_unions() && tt == eFunction && type_.eType == eUnion)
-		return true;
-	if (tt == eConstant && no_const_) {
-		return true;
-	}
-	if (!(no_func_ && tt == eFunction) &&
-			!(type_.eType == eStruct && tt == eConstant)) {
-		return false;
-	}
-	return true;
-}
-
-///////////////////////////////////////////////////
-class ParamExpressionFilter : public ExpressionFilter {
-public:
-	ParamExpressionFilter(const Type* t) : type_(t) {} 
-	virtual bool filter(int v) const;
-private:
-	const Type* type_;
-};
-
-bool
-ParamExpressionFilter::filter(int v) const
-{
-	if (!this->valid_filter())
-		return false;
-
-	if (Expression::exprTable_->filter(v))
-		return true;
-
-	eTermType tt = number_to_termtype(v, Expression::exprTable_);
-	if (tt == eConstant) {
-		return true;
-	}
-	if (tt == eFunction) {
-		if ((type_->eType == eStruct && !CGOptions::return_structs()) ||
-			(type_->eType == eUnion && !CGOptions::return_unions()))
-			return true;
-	}
-	return false;
-}
-
-
 ///////////////////////////////////////////////////////////////////////////////
 
 /*
  *
  */
 static eTermType
-ExpressionTypeProbability(const CGContext &cg_context, const ExpressionFilter *filter)
+ExpressionTypeProbability(const CGContext &cg_context, const VectorFilter *filter)
 {
 	if (cg_context.expr_depth > CGOptions::max_expr_depth())
 		return eVariable;
@@ -225,7 +116,7 @@ ExpressionTypeProbability(const CGContext &cg_context, const ExpressionFilter *f
 
 	int i = rnd_upto(100, filter);
 	ERROR_GUARD(MAX_TERM_TYPES);
-	return filter->number_to_termtype(i, Expression::exprTable_);
+	return (eTermType)(filter->lookup(i));
 }
 
 unsigned int
@@ -263,13 +154,17 @@ Expression::indented_output(std::ostream &out, int indent) const
  *
  */
 Expression *
-Expression::make_random(CGContext &cg_context, const Type* type, bool no_func, bool no_const, enum eTermType tt)
+Expression::make_random(CGContext &cg_context, const Type* type, const CVQualifiers* qfer, bool no_func, bool no_const, enum eTermType tt)
 {
 	DEPTH_GUARD_BY_TYPE_RETURN_WITH_FLAG(dtExpression, tt, NULL);
 	Expression::InitProbabilityTables();
 
 	Expression *e = 0;  
-	assert(type);
+	if (type == NULL) {
+		do { 
+			type = cg_context.get_effect_context().is_side_effect_free() ? Type::choose_random_nonvoid() : Type::choose_random_nonvoid_nonvolatile();
+		} while (type->eType == eStruct && tt == eConstant);
+	}
 	assert(!(no_func && tt == eFunction));
 	assert(!(no_const && tt == eConstant));
 	// constant struct variables can not be a subexpression?
@@ -277,7 +172,19 @@ Expression::make_random(CGContext &cg_context, const Type* type, bool no_func, b
 	 
 	// if no term type is provided, choose a random term type with restrictions
 	if (tt == MAX_TERM_TYPES) {
-		DefaultExpressionFilter filter(*type, no_func, no_const);
+		VectorFilter filter(Expression::exprTable_);
+		if (no_func || 
+			(!CGOptions::return_structs() && type->eType == eStruct) ||
+			(!CGOptions::return_unions() && type->eType == eUnion)) {
+			filter.add(eFunction);
+		}
+		// struct constants can't be subexpressions (union constant can't either?) 
+		if (no_const || type->eType == eStruct || type->eType == eUnion) {
+			filter.add(eConstant);
+		}
+		if (type->is_const_struct_union()) {
+			filter.add(eAssignment);
+		}
 		tt = ExpressionTypeProbability(cg_context, &filter); 
 	}
 	    
@@ -290,16 +197,17 @@ Expression::make_random(CGContext &cg_context, const Type* type, bool no_func, b
 		e = Constant::make_random(type);
 		break;
 	case eVariable:
-		e = ExpressionVariable::make_random(cg_context, type);
+		e = ExpressionVariable::make_random(cg_context, type, qfer);
 		break;
-#if 0
-	case eBinaryExpr:
-		e = ExpressionBinary::make_random(cg_context);
-		break;
-#endif // 0
 	case eFunction:
 		cg_context.expr_depth++;
-		e = ExpressionFuncall::make_random(cg_context, type);
+		e = ExpressionFuncall::make_random(cg_context, type, qfer);
+		break;
+	case eAssignment:
+		e = ExpressionAssign::make_random(cg_context, type, qfer);
+		break;
+	case eCommaExpr: 
+		e = ExpressionComma::make_random(cg_context, type, qfer);
 		break;
 	default: break;
 	}
@@ -325,7 +233,15 @@ Expression::make_random_param(CGContext &cg_context, const Type* type, const CVQ
 	assert(type);
 	// if a term type is provided, no need to choose random term type
 	if (tt == MAX_TERM_TYPES) {
-		ParamExpressionFilter filter(type);
+		VectorFilter filter(Expression::paramTable_);
+		filter.add(eConstant);   // no constants as function call parameters
+		if ((!CGOptions::return_structs() && type->eType == eStruct) ||
+			(!CGOptions::return_unions() && type->eType == eUnion)) {
+			filter.add(eFunction);
+		}
+		if (type->is_const_struct_union()) {
+			filter.add(eAssignment);
+		}
 		tt = ExpressionTypeProbability(cg_context, &filter);
 	}
 	 
@@ -344,6 +260,12 @@ Expression::make_random_param(CGContext &cg_context, const Type* type, const CVQ
 		cg_context.expr_depth++;
 		e = ExpressionFuncall::make_random(cg_context, type, qfer); 
 		break;
+	case eAssignment:
+		e = ExpressionAssign::make_random(cg_context, type, qfer);
+		break;
+	case eCommaExpr: 
+		e = ExpressionComma::make_random(cg_context, type, qfer);
+		break;
 	default: break;
 	} 
 
diff --git a/src/Expression.h b/src/Expression.h
index 874cef691..339408bfe 100644
--- a/src/Expression.h
+++ b/src/Expression.h
@@ -77,9 +77,11 @@ enum eTermType
 	// eUnaryExpr,
 	// eBinaryExpr,
 	eFunction,
+	eAssignment,
+	eCommaExpr,
 	eLhs
 };
-#define MAX_TERM_TYPES ((eTermType) (eFunction+1))
+#define MAX_TERM_TYPES ((eTermType) (eCommaExpr+1))
 
 template <class Key, class Value> 
 class ProbabilityTable;
@@ -91,7 +93,7 @@ class Expression
 {
 public:
 	// Factory method.
-	static Expression *make_random(CGContext &cg_context, const Type* type, bool no_func = false, bool no_const = false, enum eTermType tt=MAX_TERM_TYPES);
+	static Expression *make_random(CGContext &cg_context, const Type* type, const CVQualifiers* qfer=0, bool no_func = false, bool no_const = false, enum eTermType tt=MAX_TERM_TYPES);
 
 	static Expression *make_random_param(CGContext &cg_context, const Type* type, const CVQualifiers* qfer, enum eTermType tt=MAX_TERM_TYPES);
 
@@ -145,9 +147,9 @@ class Expression
 	enum eTermType term_type;
 	int expr_id;
 
-	static ProbabilityTable<unsigned int, eTermType> *exprTable_;
+	static ProbabilityTable<unsigned int, int> *exprTable_;
 
-	static ProbabilityTable<unsigned int, eTermType> *paramTable_;
+	static ProbabilityTable<unsigned int, int> *paramTable_;
 private:
 
 	static void InitExprProbabilityTable();
diff --git a/src/ExpressionAssign.cpp b/src/ExpressionAssign.cpp
index 342450c47..d26bb751b 100644
--- a/src/ExpressionAssign.cpp
+++ b/src/ExpressionAssign.cpp
@@ -33,7 +33,9 @@
 #include "CGContext.h"
 #include "CGOptions.h"
 #include "FactMgr.h"
+#include "Function.h"
 #include "Bookkeeper.h"
+#include "Variable.h"
 #include "StringUtils.h"
 #include "Block.h"
 
@@ -44,36 +46,18 @@
  */
 Expression *
 ExpressionAssign::make_random(CGContext &cg_context, const Type* type, const CVQualifiers* qfer)
-{
-	Expression *e = 0;
-	//++cg_context.stmt_depth;
-	//bool std_func = ExpressionFunctionProbability(cg_context);
-	//ERROR_GUARD(NULL);
- //   // unary/binary "functions" produce scalar types only
-	//if (type && (type->eType != eSimple || type->simple_type == eVoid))
-	//	std_func = false;
-
-	//Effect effect_accum = cg_context.get_accum_effect();
-	//Effect effect_stm = cg_context.get_effect_stm(); 
-	//FactMgr* fm = get_fact_mgr(&cg_context);
-	//vector<const Fact*> facts_copy = fm->global_facts; 
-	//FunctionInvocation *fi = FunctionInvocation::make_random(std_func, cg_context, type, qfer);
-	//ERROR_GUARD(NULL);
+{ 
+	StatementAssign* sa = StatementAssign::make_random(cg_context, type, qfer);
+	FactMgr* fm = get_fact_mgr(&cg_context);
+	update_fact_for_assign(sa, fm->global_facts);
+	ExpressionAssign* ea = new ExpressionAssign(sa);
+	return ea;
+}
 
-	//if (fi->failed) { 
-	//	// if it's a invalid invocation, (see FunctionInvocationUser::revisit) 
-	//	// restore the env, and replace invocation with a simple var
-	//	cg_context.reset_effect_accum(effect_accum);
-	//	cg_context.reset_effect_stm(effect_stm);
-	//	fm->restore_facts(facts_copy);
-	//	e = ExpressionVariable::make_random(cg_context, type, qfer);
-	//	delete fi;
-	//}
-	//else {
-	//	e = new ExpressionAssign(*fi);
-	//}
-	//--cg_context.stmt_depth;
-	return e;
+ExpressionAssign::ExpressionAssign(const StatementAssign* sa)
+: Expression(eAssignment),
+  assign(sa) 
+{
 }
 
 /*
@@ -81,13 +65,22 @@ ExpressionAssign::make_random(CGContext &cg_context, const Type* type, const CVQ
  */
 ExpressionAssign::~ExpressionAssign(void)
 {
-	delete &assign;
+	/*if (assign) {
+		delete assign;
+		assign = NULL;
+	}*/
+}
+
+Expression*
+ExpressionAssign::clone() const
+{
+	return new ExpressionAssign(assign);
 }
 
 CVQualifiers 
 ExpressionAssign::get_qualifiers(void) const
 { 
-	return assign.get_lhs()->get_qualifiers();
+	return assign->get_lhs()->get_qualifiers();
 }
 
 /*
@@ -96,7 +89,7 @@ ExpressionAssign::get_qualifiers(void) const
 bool
 ExpressionAssign::use_var(const Variable* v) const
 {
-	if (assign.get_lhs()->use_var(v) || assign.get_expr()->use_var(v)) {
+	if (assign->get_lhs()->use_var(v) || assign->get_expr()->use_var(v)) {
 		return true;
 	}
 	return false;
@@ -105,19 +98,19 @@ ExpressionAssign::use_var(const Variable* v) const
 bool 
 ExpressionAssign::equals(int num) const
 {
-	return assign.is_simple_assign() && assign.get_expr()->equals(num);
+	return assign->is_simple_assign() && assign->get_expr()->equals(num);
 }
 	
 bool
 ExpressionAssign::is_0_or_1(void) const
 {
-	return assign.is_simple_assign() && assign.get_expr()->is_0_or_1();
+	return assign->is_simple_assign() && assign->get_expr()->is_0_or_1();
 }
 
 bool 
 ExpressionAssign::visit_facts(vector<const Fact*>& inputs, CGContext& cg_context) const 
-{ 
-	return assign.visit_facts(inputs, cg_context);
+{
+	return assign->visit_facts(inputs, cg_context);
 }
 
 void
@@ -127,13 +120,16 @@ ExpressionAssign::Output(std::ostream &out) const
 	if (reducer && reducer->output_expr(this, out)) {
 		return;
 	} 
-	assign.Output(out, 0);
+	out << "(";
+	assign->OutputAsExpr(out);
+	out << ")";
 }
 
 void 
 ExpressionAssign::indented_output(std::ostream &out, int indent) const 
 { 
-	assign.Output(out, 0, indent);
+	output_tab(out, indent);
+	Output(out);
 }
 
 ///////////////////////////////////////////////////////////////////////////////
diff --git a/src/ExpressionAssign.h b/src/ExpressionAssign.h
index 707a0a06f..041df1d12 100644
--- a/src/ExpressionAssign.h
+++ b/src/ExpressionAssign.h
@@ -48,32 +48,36 @@ class ExpressionAssign : public Expression
 	// Factory method.
 	static Expression *make_random(CGContext &cg_context, const Type* type, const CVQualifiers* qfer=0);  
 
+	ExpressionAssign(const StatementAssign* sa);
 	virtual ~ExpressionAssign(void);  
 
+	virtual Expression *clone() const;
+
 	virtual CVQualifiers get_qualifiers(void) const;  
 
-	virtual const Type &get_type(void) const { return assign.get_lhs()->get_type();}
+	virtual const Type &get_type(void) const { return assign->get_lhs()->get_type();}
 
-	virtual void get_called_funcs(std::vector<const FunctionInvocationUser*>& funcs) const { assign.get_called_funcs(funcs);}
+	virtual void get_called_funcs(std::vector<const FunctionInvocationUser*>& funcs) const { assign->get_called_funcs(funcs);}
 
 	virtual bool visit_facts(vector<const Fact*>& inputs, CGContext& cg_context) const;
 
-	virtual bool has_uncertain_call_recursive(void) const { return assign.has_uncertain_call_recursive();} 
+	virtual bool has_uncertain_call_recursive(void) const { return assign->has_uncertain_call_recursive();} 
  
 	virtual bool use_var(const Variable* v) const;
 
 	virtual bool equals(int num) const;
 	virtual bool is_0_or_1(void) const;
 
-	virtual std::vector<const ExpressionVariable*> get_dereferenced_ptrs(void) const { return assign.get_dereferenced_ptrs();}
-	virtual void get_referenced_ptrs(std::vector<const Variable*>& ptrs) const { assign.get_referenced_ptrs(ptrs);}
+	virtual std::vector<const ExpressionVariable*> get_dereferenced_ptrs(void) const { return assign->get_dereferenced_ptrs();}
+	virtual void get_referenced_ptrs(std::vector<const Variable*>& ptrs) const { assign->get_referenced_ptrs(ptrs);}
 	
+	const Expression* get_rhs(void) const { return assign->get_rhs();}
+	const Lhs* get_lhs(void) const { return assign->get_lhs();}
 	void Output(std::ostream &) const;
 	virtual void indented_output(std::ostream &out, int indent) const;
 
 private:
-	const StatementAssign& assign;
-	explicit ExpressionAssign(const ExpressionAssign &efun);
+	const StatementAssign* assign;
 };
 
 ///////////////////////////////////////////////////////////////////////////////
diff --git a/src/ExpressionComma.cpp b/src/ExpressionComma.cpp
index b63d9bc57..f065dddfa 100644
--- a/src/ExpressionComma.cpp
+++ b/src/ExpressionComma.cpp
@@ -42,38 +42,21 @@
 /*
  *
  */
-Expression *
+ExpressionComma*
 ExpressionComma::make_random(CGContext &cg_context, const Type* type, const CVQualifiers* qfer)
 {
-	Expression *e = 0;
-	//++cg_context.stmt_depth;
-	//bool std_func = ExpressionFunctionProbability(cg_context);
-	//ERROR_GUARD(NULL);
- //   // unary/binary "functions" produce scalar types only
-	//if (type && (type->eType != eSimple || type->simple_type == eVoid))
-	//	std_func = false;
-
-	//Effect effect_accum = cg_context.get_accum_effect();
-	//Effect effect_stm = cg_context.get_effect_stm(); 
-	//FactMgr* fm = get_fact_mgr(&cg_context);
-	//vector<const Fact*> facts_copy = fm->global_facts; 
-	//FunctionInvocation *fi = FunctionInvocation::make_random(std_func, cg_context, type, qfer);
-	//ERROR_GUARD(NULL);
+	Expression* lhs = Expression::make_random(cg_context, NULL, NULL, false, true);
+	Expression* rhs = Expression::make_random(cg_context, type, qfer, false, false);
+	ExpressionComma* ec = new ExpressionComma(*lhs, *rhs);
+	return ec;
+}
 
-	//if (fi->failed) { 
-	//	// if it's a invalid invocation, (see FunctionInvocationUser::revisit) 
-	//	// restore the env, and replace invocation with a simple var
-	//	cg_context.reset_effect_accum(effect_accum);
-	//	cg_context.reset_effect_stm(effect_stm);
-	//	fm->restore_facts(facts_copy);
-	//	e = ExpressionVariable::make_random(cg_context, type, qfer);
-	//	delete fi;
-	//}
-	//else {
-	//	e = new ExpressionComma(*fi);
-	//}
-	//--cg_context.stmt_depth;
-	return e;
+ExpressionComma::ExpressionComma(const Expression& l, const Expression& r)
+	: Expression(eCommaExpr),
+	  lhs(l),
+	  rhs(r)
+{
+	// nothing else to do
 }
 
 /*
@@ -85,6 +68,12 @@ ExpressionComma::~ExpressionComma(void)
 	delete &rhs;
 }
 
+Expression*
+ExpressionComma::clone(void) const
+{
+	return new ExpressionComma(*lhs.clone(), *rhs.clone());
+}
+
 bool 
 ExpressionComma::visit_facts(vector<const Fact*>& inputs, CGContext& cg_context) const 
 {
@@ -110,8 +99,11 @@ ExpressionComma::Output(std::ostream &out) const
 	if (reducer && reducer->output_expr(this, out)) {
 		return;
 	} 
+	out << "(";
 	lhs.Output(out);
+	out << " , ";
 	rhs.Output(out);
+	out << ")";
 }
 
 void 
diff --git a/src/ExpressionComma.h b/src/ExpressionComma.h
index 2616fece2..47dfdb812 100644
--- a/src/ExpressionComma.h
+++ b/src/ExpressionComma.h
@@ -41,10 +41,12 @@ class ExpressionComma : public Expression
 {
 public:
 	// Factory method.
-	static Expression *make_random(CGContext &cg_context, const Type* type, const CVQualifiers* qfer=0);  
+	static ExpressionComma *make_random(CGContext &cg_context, const Type* type, const CVQualifiers* qfer=0);  
 
 	virtual ~ExpressionComma(void);  
 
+	Expression* clone(void) const;
+
 	virtual CVQualifiers get_qualifiers(void) const { return rhs.get_qualifiers();}  
 
 	virtual const Type &get_type(void) const { return rhs.get_type();}
@@ -63,13 +65,15 @@ class ExpressionComma : public Expression
 	virtual std::vector<const ExpressionVariable*> get_dereferenced_ptrs(void) const;
 	virtual void get_referenced_ptrs(std::vector<const Variable*>& ptrs) const { lhs.get_referenced_ptrs(ptrs); rhs.get_referenced_ptrs(ptrs);}
 	
+	const Expression* get_lhs(void) const { return &lhs;}
+	const Expression* get_rhs(void) const { return &rhs;}
 	void Output(std::ostream &) const;
 	virtual void indented_output(std::ostream &out, int indent) const;
 
 private:
 	const Expression& lhs;
 	const Expression& rhs;
-	explicit ExpressionComma(const ExpressionComma &e);
+	explicit ExpressionComma(const Expression& l, const Expression& r);
 };
 
 ///////////////////////////////////////////////////////////////////////////////
diff --git a/src/Fact.h b/src/Fact.h
index afa07e923..52f574f3a 100644
--- a/src/Fact.h
+++ b/src/Fact.h
@@ -91,7 +91,7 @@ class Fact
 
 	virtual std::vector<const Fact*> abstract_fact_for_assign(const std::vector<const Fact*>& /*facts*/, const Lhs* /*lhs*/, const Expression* /*rhs*/) = 0;
 
-	virtual Fact* abstract_fact_for_return(const std::vector<const Fact*>& /*facts*/, const ExpressionVariable* /*var*/, const Function* /*func*/) {return 0;};
+	virtual std::vector<const Fact*> abstract_fact_for_return(const std::vector<const Fact*>& /*facts*/, const ExpressionVariable* /*var*/, const Function* /*func*/) = 0;
 
 	static void doFinalization();
 
diff --git a/src/FactMgr.cpp b/src/FactMgr.cpp
index 588d3e113..b32a625ad 100644
--- a/src/FactMgr.cpp
+++ b/src/FactMgr.cpp
@@ -127,7 +127,7 @@ add_new_var_fact(const Variable* v, FactVec& facts)
 	const vector<Fact*>& meta_facts = FactMgr::meta_facts;
 	assert(v);
 	// TODO: consider facts related to struct or arrays
-	if (v->type && (v->type->eType == eSimple || v->type->eType == ePointer || v->type->eType == eUnion) && v->init) { 
+	if (v->type && (v->type->eType == eSimple || v->type->eType == ePointer || v->type->eType == eUnion)) { 
 		FactVec tmp_facts;
 		for (j=0; j<meta_facts.size(); j++) {
 			Lhs lhs(*v);
@@ -195,7 +195,7 @@ update_facts_for_oos_vars(const vector<Variable*>& vars, FactVec& facts)
 			//print_facts(facts);
 			// remove all facts related to this variable
 			const Fact* f = facts[j];
-			if (f->get_var() == var) {
+			if (var->match(f->get_var())) {
 				facts.erase(facts.begin() + j);
 				len--;
 				j--;
@@ -230,7 +230,7 @@ update_facts_for_oos_vars(const vector<const Variable*>& vars, FactVec& facts)
 			//print_facts(facts);
 			// remove all facts related to this variable
 			const Fact* f = facts[j];
-			if (f->get_var() == var) {
+			if (var->match(f->get_var())) {
 				facts.erase(facts.begin() + j);
 				len--;
 				j--;
@@ -268,7 +268,7 @@ remove_function_local_facts(std::vector<const Fact*>& inputs, const Statement* s
 		const Variable* v = inputs[i]->get_var();
 		// if it's fact for a local variable of this function, or return variable
 		// of another function, we are not interested in them after exit function
-		if (func->is_var_on_stack(v, stm) || (v->is_rv() && v != func->rv)) { 
+		if (func->is_var_on_stack(v, stm) || (v->is_rv() && !func->rv->match(v))) { 
 			inputs.erase(inputs.begin() + i);
 			i--;
 			len--; 
@@ -448,7 +448,7 @@ void FactMgr::remove_rv_facts(FactVec& facts)
 	size_t len = facts.size();
 	for (size_t i=0; i<len; i++) { 
 		const Fact* f = facts[i]; 
-		if (f->get_var()->is_rv() && f->get_var() != func->rv) {
+		if (f->get_var()->is_rv() && !func->rv->match(f->get_var())) {
 			facts.erase(facts.begin() + i);
 			len--;
 			i--; 
@@ -493,19 +493,19 @@ update_fact_for_assign(const StatementAssign* sa, FactVec& inputs)
 void 
 update_fact_for_return(const StatementReturn* sr, FactVec& inputs)
 {
-	size_t i;
+	size_t i, j;
     for (i=0; i<FactMgr::meta_facts.size(); i++) {
-        Fact* f = FactMgr::meta_facts[i]->abstract_fact_for_return(inputs, sr->get_var(), sr->func);
-		if (f) {
+        std::vector<const Fact*> facts = FactMgr::meta_facts[i]->abstract_fact_for_return(inputs, sr->get_var(), sr->func);
+		for (j=0; j<facts.size(); j++) {
 			// merge with other return statements
-			merge_fact(inputs, f);
-			sr->func->fact_changed = true;
+			if (merge_fact(inputs, facts[j])) {
+				sr->func->fact_changed = true;
+			}
 		}
     }
 	// incorporate current facts into return facts
 	FactMgr* fm = get_fact_mgr_for_func(sr->func);
 	fm->set_fact_out(sr, inputs);
-	//merge_facts(fm->return_facts, fm->map_facts_out[sr]);
 }
 
 void
@@ -606,11 +606,14 @@ FactMgr::makeup_new_var_facts(vector<const Fact*>& old_facts, const vector<const
     size_t i; 
     for (i=0; i<new_facts.size(); i++) { 
 		const Fact* f = new_facts[i];
-		// if there are variable facts not present in old facts,
-		// mean they are variables created after old_facts,
-		// manually add them
-		if (find_related_fact(old_facts, f) == 0) { 
-			add_new_var_fact(f->get_var(), old_facts);
+		const Variable* v = f->get_var();
+		if (v->is_global() || v->is_local()) { 
+			// if there are variable facts not present in old facts,
+			// mean they are variables created after old_facts,
+			// manually add them
+			if (find_related_fact(old_facts, f) == 0) { 
+				add_new_var_fact(v, old_facts);
+			}
 		}
 	}
 }
@@ -805,22 +808,6 @@ merge_jump_facts(FactVec& facts, const FactVec& jump_facts)
     return changed;
 }
 
-bool
-merge_prev_facts(FactVec& facts, FactVec& old_facts)
-{ 
-    size_t i; 
-    for (i=0; i<facts.size(); i++) { 
-		const Fact* f = facts[i];
-		// if there are variable facts not present in old facts,
-		// mean they are variables created after old_facts,
-		// manually add them before we do a merge
-		if (find_related_fact(old_facts, f) == 0) {
-			add_new_var_fact(f->get_var(), old_facts);
-		}
-	}
-	return merge_facts(facts, old_facts);
-}
-
 bool
 renew_facts(FactVec& facts, const FactVec& new_facts)
 { 
@@ -983,7 +970,7 @@ FactMgr::find_updated_final_facts(const Statement* stm, vector<Fact*>& facts)
 		Fact* f = facts_out[i];
 		// sometimes there is no pre-facts for return variables, so we don't
 		// check the difference
-		if (f->get_var() == func->rv) {
+		if (func->rv->match(f->get_var())) {
 			facts.push_back(f);
 		} 
 		else {
@@ -1056,7 +1043,7 @@ FactMgr::sanity_check_map() const
 		const vector<const Fact*>& facts = iter->second;
 		for (size_t i=0; i<facts.size(); i++) {
 			const Variable* v = facts[i]->get_var();
-			if (!v->is_visible(stm->parent) && v != func->rv) {
+			if (!v->is_visible(stm->parent) && !func->rv->match(v)) {
 				//assert(0);
 			}
 		}
diff --git a/src/FactMgr.h b/src/FactMgr.h
index 4f4689149..db0f48992 100644
--- a/src/FactMgr.h
+++ b/src/FactMgr.h
@@ -160,9 +160,6 @@ bool merge_facts(FactVec& facts, const FactVec& new_facts);
 /* merge two facts env */
 bool merge_jump_facts(FactVec& facts, const FactVec& jump_facts);
 
-/* merge one env with a prev env that may miss new variables created recently */
-bool merge_prev_facts(FactVec& facts, FactVec& old_facts);
-
 /* check if two facts env are identical */
 bool same_facts(const FactVec& facts1, const FactVec& facts2);
 
diff --git a/src/FactPointTo.cpp b/src/FactPointTo.cpp
index 7cdcc159b..ed673c33a 100644
--- a/src/FactPointTo.cpp
+++ b/src/FactPointTo.cpp
@@ -41,6 +41,8 @@
 #include "Function.h"
 #include "ExpressionVariable.h"
 #include "ExpressionFuncall.h"
+#include "ExpressionAssign.h"
+#include "ExpressionComma.h"
 #include "FunctionInvocation.h"
 #include "FunctionInvocationUser.h"
 #include "FactMgr.h"
@@ -167,119 +169,137 @@ FactPointTo::size() const
 	return point_to_vars.size();
 }
 
-std::vector<const Fact*>
-FactPointTo::abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* rhs)
-{   
-	std::vector<const Fact*> ret_facts;
-	// special case: the first union field is a pointer, and is initialized by a string initializer
-	// JYTODO: uncomment and fix an assertin failure it causes
-	if (lhs->get_var()->type->eType == eUnion && lhs->get_indirect_level() == 0) {
-		/*assert(!lhs->get_var()->field_vars.empty()); 
-		const Variable* f1 = lhs->get_var()->field_vars[0];
-		if (f1->type->eType == ePointer && rhs->term_type == eConstant) {
-			Lhs tmp(*f1);
-			return abstract_fact_for_assign(facts, &tmp, rhs);
-		}*/
+vector<const Fact*>
+FactPointTo::rhs_to_lhs_transfer(const vector<const Fact*>& facts, const vector<const Variable*>& lvars, const Expression* rhs)
+{
+	vector<const Fact*> empty;
+	if (lvars.size()==0) return empty;
+	// assert all possible LHS are pointers
+	for (size_t i=0; i<lvars.size(); i++) {
+		assert(lvars[i]->type->eType == ePointer);
+	} 
+	if (rhs == NULL) {
+		return FactPointTo::make_facts(lvars, garbage_ptr);
 	}
-	// return empty set if lhs is not pointer
-	if (lhs->get_type().eType != ePointer) {
-		return ret_facts;
+	if (rhs->get_type().eType != ePointer && rhs->get_type().eType != eUnion) { 
+		if (rhs->equals(0) && rhs->get_type().SizeInBytes() != SIZE_UNKNOWN && rhs->get_type().SizeInBytes() >= 8) {
+			return FactPointTo::make_facts(lvars,  null_ptr);
+		} else { 
+			return FactPointTo::make_facts(lvars, garbage_ptr);
+		}
+	}
+	if (rhs->term_type == eConstant) {  
+		const Constant* c = dynamic_cast<const Constant*>(rhs);  
+		if (rhs->get_type().eType == ePointer) {
+			return FactPointTo::make_facts(lvars, rhs->equals(0) ? null_ptr : garbage_ptr);
+		}
+		// for unions, all pointer fields are equally initialized if the 1st field is pointer
+		else if (rhs->get_type().eType == eUnion) {
+			if (lvars[0]->field_var_of->type->eType == eUnion && lvars[0]->get_field_id() == 0 && c->get_field(0)=="0") {
+				return FactPointTo::make_facts(lvars, null_ptr);
+			} else {
+				return FactPointTo::make_facts(lvars, garbage_ptr);
+			}
+		}
+		else {
+			// remove this when we add pointer fields to structs later
+			assert(0);
+		}
 	}
-	// find all the pointed variables on LHS
-	std::vector<const Variable*> lvars = merge_pointees_of_pointer(lhs->get_var()->get_collective(), lhs->get_indirect_level(), facts);
-	  
-    if (rhs->term_type == eConstant) { 
-        string v = ((const Constant*)rhs)->get_value(); 
-        if (v.compare("0") == 0) {
-            return FactPointTo::make_facts(lvars, null_ptr); 
-        }
-        else {
-            // what does it mean to set a pointer to a non-zero constant?
-            // there could be multiple interpretations. Right now we just choose
-            // the simplest one: treat it as zero
-            return FactPointTo::make_facts(lvars, null_ptr); 
-        }
-    } 
     else if (rhs->term_type == eVariable) {
-        const ExpressionVariable* expvar = (const ExpressionVariable*)rhs;
+		const ExpressionVariable* expvar = (const ExpressionVariable*)rhs;
 		int indirect = expvar->get_indirect_level();
-        if (indirect < 0) {
-            // taking address of another variable. multi-level indirection is not allowed
+		if (indirect < 0) {
+			// taking address of another variable. multi-level indirection is not allowed
 			assert(indirect == -1);
 			return FactPointTo::make_facts(lvars, expvar->get_var()->get_collective()); 
-        }
-		else if (indirect > 0) { 
+		} 
+		if (rhs->get_type().is_aggregate()) {
+			vector<const Variable*> vars = merge_pointees_of_pointer(expvar->get_var()->get_collective(), indirect, facts);
+			FactVec ret_facts;
+			for (size_t i=0; i<vars.size(); i++) {
+				vector<const Variable*> pointers;
+				vars[i]->find_pointer_fields(pointers);
+				assert(lvars.size() == pointers.size());
+				for (size_t j=0; j<lvars.size(); j++) { 
+					const FactPointTo* fp = FactPointTo::make_fact(lvars[j], merge_pointees_of_pointer(pointers[j], 1, facts));
+					merge_fact(ret_facts, fp);
+				}
+			}
+			return ret_facts;
+		}
+		else { 
 			vector<const Variable*> var_set = merge_pointees_of_pointer(expvar->get_var()->get_collective(), indirect+1, facts);
 			return FactPointTo::make_facts(lvars, var_set);
 		}
-        else {
-			const Variable* pointer = expvar->get_var()->get_collective();
-            FactPointTo dummy(pointer);
-            const Fact* exist_fact = find_related_fact(facts, &dummy);
-            // we are setting a pointer to another pointer that hasn't
-            // been initialized in this function, most likely it's a argument
-            if (exist_fact == 0) {
-                assert(0); //return pointer->is_argument() ? FactPointTo::make_facts(lvars, tbd_ptr) : FactPointTo::make_facts(lvars, garbage_ptr);
-            } 
-            // otherwise use the analysis for the existing pointer
-            else {
-                FactPointTo* f2 = (FactPointTo*)exist_fact;
-                return FactPointTo::make_facts(lvars, f2->get_point_to_vars());
-            } 
-        }
-    }
-    else if (rhs->term_type == eFunction) {
-        const ExpressionFuncall* funcall = (const ExpressionFuncall*)rhs;
-        const FunctionInvocation* fi = funcall->get_invoke();
-        switch (fi->invoke_type) {
-            case eBinaryPrim:
-            case eUnaryPrim:
-                break;              // TODO: support pointer arithmatics
-            case eFuncCall: {
-				const FunctionInvocationUser* fiu = dynamic_cast<const FunctionInvocationUser*>(fi);
+	} 
+    else if (rhs->term_type == eFunction) {  
+        const FunctionInvocation* fi = rhs->get_invoke();
+		assert(fi);
+		// TODO: support pointer arithmetics
+        if (fi->invoke_type == eFuncCall) {  
+			const FunctionInvocationUser* fiu = dynamic_cast<const FunctionInvocationUser*>(fi);
+			if (fiu->get_type().is_aggregate()) {
+				FactVec ret_facts;
+				vector<const Variable*> pointers;
+				fiu->get_func()->rv->find_pointer_fields(pointers);
+				for (size_t i=0; i<lvars.size(); i++) {
+					const FactPointTo* rv_fact = dynamic_cast<const FactPointTo*>(get_return_fact_for_invocation(fiu, pointers[i], ePointTo));
+					const FactPointTo* fp = FactPointTo::make_fact(lvars[i], rv_fact->get_point_to_vars());
+					ret_facts.push_back(fp);
+				}
+				return ret_facts;
+			} 
+			else {
 				// find the fact regarding return variable
-				const FactPointTo* rv_fact = (const FactPointTo*)(get_return_fact_for_invocation(fiu, ePointTo)); 
+				const FactPointTo* rv_fact = dynamic_cast<const FactPointTo*>(get_return_fact_for_invocation(fiu, fiu->get_func()->rv, ePointTo)); 
 				assert(rv_fact);
 				return FactPointTo::make_facts(lvars, rv_fact->get_point_to_vars());
-            }
+			}
         }
     } 
+	else if (rhs->term_type == eAssignment) {
+		const ExpressionAssign* ea = dynamic_cast<const ExpressionAssign*>(rhs);
+		return rhs_to_lhs_transfer(facts, lvars, ea->get_rhs());
+	}
+	else if (rhs->term_type == eCommaExpr) {
+		const ExpressionComma* ec = dynamic_cast<const ExpressionComma*>(rhs);
+		return rhs_to_lhs_transfer(facts, lvars, ec->get_rhs());
+	}
+	return empty;
+}
+
+std::vector<const Fact*>
+FactPointTo::abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* rhs)
+{   
+	std::vector<const Fact*> ret_facts;
+	
+	// find all the pointed variables on LHS
+	vector<const Variable*> lvars = merge_pointees_of_pointer(lhs->get_var()->get_collective(), lhs->get_indirect_level(), facts); 
+	// return empty set if lhs is not pointer
+	if (lhs->get_type().eType == ePointer) {  
+		return rhs_to_lhs_transfer(facts, lvars, rhs);
+	} 
+	for (size_t i=0; i<lvars.size(); i++) {
+		const Variable* v = lvars[i]; 
+		if (v->is_inside_union_field()) {
+			for (; v && v->type->eType != eUnion; v = v->field_var_of);
+			assert(v && v->type->eType == eUnion);
+		}
+		vector<const Variable*> pointers;
+		v->find_pointer_fields(pointers);
+		// transfer facts for pointer fields
+		FactVec new_facts = rhs_to_lhs_transfer(facts, pointers, rhs);
+		ret_facts.insert(ret_facts.end(), new_facts.begin(), new_facts.end());
+	}
     return ret_facts;
 }
 
-Fact* 
+std::vector<const Fact*>
 FactPointTo::abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* var, const Function* func)
 { 
-    if (func->return_type->eType == ePointer) {
-		int indirect_level = var->get_indirect_level();
-		// if > -2, means we "return &(&v)", which shouldn't happen in current impl.
-	    assert(indirect_level > -2);  
-		if (indirect_level == -1) {
-			return FactPointTo::make_fact(func->rv, var->get_var()->get_collective());
-		}
-		if (indirect_level == 0) {
-			FactPointTo dummy(var->get_var()->get_collective());
-			const Fact* exist_fact = find_related_fact(facts, &dummy);
-              
-			if (exist_fact == 0) { 
-				// we are returning a pointer we knew nothing, something is wrong
-				assert(0);
-			}
-			else { 
-				return FactPointTo::make_fact(func->rv, ((FactPointTo*)exist_fact)->get_point_to_vars());
-			}
-		}
-		else {
-			// for one or more level(s) of dereferences 
-			// this is a much complicated case: we are returning a pointer in the form of *p (which implies 
-			// p is a double pointer), we need to find out all variables p point to, and merge all variables
-			// these variables in turn point to 
-			vector<const Variable*> var_set = merge_pointees_of_pointer(var->get_var()->get_collective(), indirect_level+1, facts);			
-			return FactPointTo::make_fact(func->rv, var_set);
-		}
-
-    }
-    return 0;
+	Lhs lhs(*func->rv);
+	return abstract_fact_for_assign(facts, &lhs, var);
 }
 
 Fact*
@@ -401,7 +421,7 @@ bool
 FactPointTo::point_to(const Variable* v) const 
 { 
 	for (size_t i=0; i<point_to_vars.size(); i++) {
-		if (v->match(point_to_vars[i])) {
+		if (v->loose_match(point_to_vars[i]) || point_to_vars[i]->loose_match(v)) {
 			return true;
 		}
 	}
@@ -492,7 +512,7 @@ bool FactPointTo::is_pointing_to_locals(const Variable* v, const Block* b, int i
 		return v->is_visible_local(b);
 	}
 	if (!v->is_pointer()) return false;
-	if (v->isArray) {
+	if (v->isArray || v->is_array_field()) {
 		v = v->get_collective();
 	}
 	vector<const Variable*> pointees;
@@ -677,7 +697,9 @@ FactPointTo::Output(std::ostream &out) const
 bool 
 FactPointTo::is_assertable(const Statement* stm) const
 {
-	return !is_variable_in_set(point_to_vars, garbage_ptr) &&
+	string dummy;
+	return (var->get_array(dummy) == NULL) &&
+		   !is_variable_in_set(point_to_vars, garbage_ptr) &&
 		   !is_variable_in_set(point_to_vars, tbd_ptr) && 
 		   !has_invisible(stm);
 }
@@ -701,11 +723,12 @@ FactPointTo::merge_pointees_of_pointers(const std::vector<const Variable*>& ptrs
 	vector<const Variable*> pointee_vars;
 	for (i=0; i<ptrs.size(); i++) {
 		const Variable* p = ptrs[i];
+		if (FactPointTo::is_special_ptr(p)) continue;
 		FactPointTo dummy(p);
 		const FactPointTo* exist_fact = (const FactPointTo*)find_related_fact(facts, &dummy);
 		// I can not think of a reason this is null
 		// well...this actually happens when p is a parameter of function f, and we are in the middle of creating f 
-		// assert(exist_fact);
+		assert(exist_fact);
 		if (exist_fact) {
 			for (j=0; j<exist_fact->get_point_to_vars().size(); j++) {
 				const Variable* pointee = exist_fact->get_point_to_vars()[j];
diff --git a/src/FactPointTo.h b/src/FactPointTo.h
index a2c2ae6cb..ed96abe78 100644
--- a/src/FactPointTo.h
+++ b/src/FactPointTo.h
@@ -69,8 +69,9 @@ class FactPointTo : public Fact
 	bool is_dead(void) const;
 	bool has_invisible(const Statement* stm) const;
 	int  size() const;
-	virtual std::vector<const Fact*> abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* rhs);
-	virtual Fact* abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* var, const Function* func);
+	std::vector<const Fact*> rhs_to_lhs_transfer(const std::vector<const Fact*>& facts, const vector<const Variable*>& lvars, const Expression* rhs);
+	virtual vector<const Fact*> abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* rhs);
+	virtual vector<const Fact*> abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* var, const Function* func);
 
 	FactPointTo* mark_dead_var(const Variable* v);
 	FactPointTo* mark_func_end(const Statement* stm);
diff --git a/src/FactUnion.cpp b/src/FactUnion.cpp
index 146f06d96..005a8ac10 100644
--- a/src/FactUnion.cpp
+++ b/src/FactUnion.cpp
@@ -39,6 +39,8 @@
 #include "Lhs.h"
 #include "ExpressionVariable.h"
 #include "FunctionInvocationUser.h"
+#include "ExpressionAssign.h"
+#include "ExpressionComma.h"
 #include <assert.h> 
 
 const int  FactUnion::TOP = -2;
@@ -79,7 +81,8 @@ FactUnion::rhs_to_lhs_transfer(const std::vector<const Fact*>& facts, const vect
 	// assert all possible LHS are unions
 	for (size_t i=0; i<lvars.size(); i++) {
 		assert(lvars[i]->type->eType == eUnion);
-	}
+	} 
+	assert(rhs != NULL);
 	if (rhs->term_type == eConstant) {  
 		return make_facts(lvars, 0); 
 	}
@@ -99,11 +102,19 @@ FactUnion::rhs_to_lhs_transfer(const std::vector<const Fact*>& facts, const vect
 		if (fi->invoke_type == eFuncCall) { 
 			const FunctionInvocationUser* fiu = dynamic_cast<const FunctionInvocationUser*>(fi);
 			// find the fact regarding return variable
-			const FactUnion* rv_fact = dynamic_cast<const FactUnion*>(get_return_fact_for_invocation(fiu, eUnionWrite)); 
+			const FactUnion* rv_fact = dynamic_cast<const FactUnion*>(get_return_fact_for_invocation(fiu, fiu->get_func()->rv, eUnionWrite)); 
 			assert(rv_fact);
 			return make_facts(lvars, rv_fact->get_last_written_fid());
         }
     } 
+	else if (rhs->term_type == eAssignment) {
+		const ExpressionAssign* ea = dynamic_cast<const ExpressionAssign*>(rhs);
+		return rhs_to_lhs_transfer(facts, lvars, ea->get_rhs());
+	}
+	else if (rhs->term_type == eCommaExpr) {
+		const ExpressionComma* ec = dynamic_cast<const ExpressionComma*>(rhs);
+		return rhs_to_lhs_transfer(facts, lvars, ec->get_rhs());
+	}
 	return empty;
 }
 
@@ -112,6 +123,7 @@ std::vector<const Fact*>
 FactUnion::abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* rhs)
 {   
 	std::vector<const Fact*> ret_facts; 
+	if (rhs == NULL) return ret_facts;
 	// find all the pointed variables on LHS
 	std::vector<const Variable*> lvars = FactPointTo::merge_pointees_of_pointer(lhs->get_var()->get_collective(), lhs->get_indirect_level(), facts);
 	if (lhs->get_type().eType == eUnion) {
@@ -132,19 +144,20 @@ FactUnion::abstract_fact_for_assign(const std::vector<const Fact*>& facts, const
 }
 
 /* draw facts from return statement */
-Fact* 
+std::vector<const Fact*>
 FactUnion::abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* rv, const Function* func)
 {
+	vector<const Fact*> ret_facts;
     if (func->return_type->eType == eUnion) {
 		int indirect = rv->get_indirect_level(); 
 	    assert(indirect >= 0);   
 		vector<const Variable*> rvars = FactPointTo::merge_pointees_of_pointer(rv->get_var()->get_collective(), indirect, facts);
 		const FactUnion* rhs_fact = dynamic_cast<const FactUnion*>(join_var_facts(facts, rvars)); 
 		if (rhs_fact) {
-			return make_fact(func->rv, rhs_fact->get_last_written_fid());
+			ret_facts.push_back(make_fact(func->rv, rhs_fact->get_last_written_fid()));
 		}
 	}
-    return 0;
+    return ret_facts;
 }
 
 Fact*
@@ -178,7 +191,9 @@ FactUnion::make_facts(const vector<const Variable*>& vars, int fid)
 bool 
 FactUnion::is_nonreadable_field(const Variable *v, const std::vector<const Fact*>& facts)
 {
-	if (v->is_union_field()) {
+	if (v->is_inside_union_field()) {
+		for (; v && !v->is_union_field(); v = v->field_var_of);
+		assert(v->is_union_field());
 		FactUnion tmp(v->field_var_of, v->get_field_id());
 		const FactUnion* fu = dynamic_cast<const FactUnion*>(find_related_fact(facts, &tmp));
 		if (fu && !tmp.imply(*fu)) {
@@ -278,7 +293,7 @@ FactUnion::imply(const Fact& f) const
 bool
 FactUnion::is_field_readable(const Variable* v, int fid, const vector<const Fact*>& facts)
 {
-	assert(v->type->eType == eUnion && fid >=0 && fid < v->type->fields.size());
+	assert(v->type->eType == eUnion && fid >=0 && fid < (int)(v->type->fields.size()));
 	FactUnion tmp(v, fid);
 	const FactUnion* fu = dynamic_cast<const FactUnion*>(find_related_fact(facts, &tmp));
 	return (fu && tmp.imply(*fu)) ;
diff --git a/src/FactUnion.h b/src/FactUnion.h
index 241745182..387563bb3 100644
--- a/src/FactUnion.h
+++ b/src/FactUnion.h
@@ -73,7 +73,7 @@ class FactUnion : public Fact
 	// transfer functions
 	vector<const Fact*> rhs_to_lhs_transfer(const vector<const Fact*>& facts, const vector<const Variable*>& lvars, const Expression* rhs);
 	virtual vector<const Fact*> abstract_fact_for_assign(const std::vector<const Fact*>& facts, const Lhs* lhs, const Expression* /*rhs*/);
-	virtual Fact* abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* rv, const Function* func);
+	virtual vector<const Fact*> abstract_fact_for_return(const std::vector<const Fact*>& facts, const ExpressionVariable* rv, const Function* func);
 	virtual Fact* join_var_facts(const vector<const Fact*>& facts, const vector<const Variable*>& vars) const;
 	virtual Fact* clone(void) const;
 
diff --git a/src/Filter.cpp b/src/Filter.cpp
index 96cf024df..6b7179586 100644
--- a/src/Filter.cpp
+++ b/src/Filter.cpp
@@ -73,8 +73,7 @@ Filter::current_kind(void) const
 		return fDefault;
 	else if (CGOptions::dfs_exhaustive())
 		return fDFS;
-
-	assert(0);
+	return MAX_FILTER_KIND_SIZE;
 }
 
 /*
diff --git a/src/Function.cpp b/src/Function.cpp
index f9e222494..f1c5b0d35 100644
--- a/src/Function.cpp
+++ b/src/Function.cpp
@@ -351,7 +351,7 @@ Function::make_random_signature(const CGContext& cg_context, const Type* type, c
 	CVQualifiers ret_qfer = qfer==0 ? CVQualifiers::random_qualifiers(type, Effect::READ, cg_context, true) 
 		                            : qfer->random_qualifiers(true, Effect::READ, cg_context);
 	ERROR_GUARD(NULL);
-	f->rv = VariableSelector::make_dummy_variable(rvname, type, &ret_qfer);
+	f->rv = Variable::CreateVariable(rvname, type, NULL, &ret_qfer);
 	GenerateParameterList(*f); 
 	FMList.push_back(new FactMgr(f));
 	return f;
@@ -384,7 +384,7 @@ Function::make_first(void)
 	string rvname = f->name + "_" + "rv"; 
 	CVQualifiers ret_qfer = CVQualifiers::random_qualifiers(ty); 
 	ERROR_GUARD(NULL);
-	f->rv = VariableSelector::make_dummy_variable(rvname, ty, &ret_qfer);
+	f->rv = Variable::CreateVariable(rvname, ty, NULL, &ret_qfer);
 
 	// create a fact manager for this function, with empty global facts 
 	FactMgr* fm = new FactMgr(f);
diff --git a/src/FunctionInvocation.cpp b/src/FunctionInvocation.cpp
index cbd6269de..7307712ec 100644
--- a/src/FunctionInvocation.cpp
+++ b/src/FunctionInvocation.cpp
@@ -214,7 +214,7 @@ FunctionInvocation::make_random_binary(CGContext &cg_context, const Type* type)
 			if (!not_constant) {
 				rhs = Constant::make_random_upto(lhs_type->SizeInBytes() * 8);
 			} else {
-				rhs = Expression::make_random(rhs_cg_context, rhs_type, false, true, tt);
+				rhs = Expression::make_random(rhs_cg_context, rhs_type, NULL, false, true, tt);
 			}
 		}
 		else {
@@ -242,7 +242,8 @@ FunctionInvocation::make_random_binary(CGContext &cg_context, const Type* type)
 
 	// ordered operators such as "||" or "&&" may skip the 2nd parameter
 	if (IsOrderedStandardFunc(op)) {
-		merge_prev_facts(fm->global_facts, facts_copy);
+		fm->makeup_new_var_facts(facts_copy, fm->global_facts);
+		merge_facts(fm->global_facts, facts_copy);
 	}
 	// TODO: fix `rhs' for eLShift and eRShift and ...
 	// Currently, the "fix" is handled in `FunctionInvocationBinary::Output'.
@@ -269,7 +270,7 @@ FunctionInvocation::make_random_binary_ptr_comparison(CGContext &cg_context)
 	Effect lhs_eff_accum;
 	CGContext lhs_cg_context(cg_context, cg_context.get_effect_context(), &lhs_eff_accum);
 	lhs_cg_context.flags |= NO_DANGLING_PTR;
-	Expression *lhs = Expression::make_random(lhs_cg_context, type, true);
+	Expression *lhs = Expression::make_random(lhs_cg_context, type, 0, true);
 	ERROR_GUARD_AND_DEL1(NULL, fi);
 	cg_context.add_effect(lhs_eff_accum);
 
@@ -284,12 +285,12 @@ FunctionInvocation::make_random_binary_ptr_comparison(CGContext &cg_context)
 	// If we are guaranteed that the LHS will be evaluated before the RHS,
 	// or if the LHS is pure (not merely side-effect-free),
 	// then we can generate the RHS under the original effect context.
-	if (IsOrderedStandardFunc(op) || lhs_eff_accum.is_pure()) {
+	if (IsOrderedStandardFunc(op)) { //  lhs_eff_accum.is_pure())  JYTODO: purity needs to be redefined
 		// although we don't need care about other side effect, we do
 		// need to pass in NO_DANGLING_PTR flag
 		unsigned int old_flag = cg_context.flags;
 		cg_context.flags |= NO_DANGLING_PTR;
-		rhs = Expression::make_random(cg_context, type, true, false, tt);
+		rhs = Expression::make_random(cg_context, type, 0, true, false, tt);
 		cg_context.flags = old_flag;
 	} else {
 		// Otherwise, the RHS must be generated under the combined effect
@@ -300,7 +301,7 @@ FunctionInvocation::make_random_binary_ptr_comparison(CGContext &cg_context)
 
 		CGContext rhs_cg_context(cg_context, rhs_eff_context, &rhs_eff_accum);
 		rhs_cg_context.flags |= NO_DANGLING_PTR;
-		rhs = Expression::make_random(rhs_cg_context, type, true, false, tt);
+		rhs = Expression::make_random(rhs_cg_context, type, 0, true, false, tt);
 		cg_context.add_effect(rhs_eff_accum);
 	}
 	ERROR_GUARD_AND_DEL2(NULL, fi, lhs);
@@ -488,8 +489,8 @@ FunctionInvocation::visit_facts(vector<const Fact*>& inputs, CGContext& cg_conte
 			CGContext param_cg_context(cg_context, running_eff_context, &param_eff_accum);
 			// the parameters might be function calls
 			const Expression* value = param_value[i];
-			if (h == 3659)
-				BREAK_NOP;		// for debugging
+			if (h == 236)
+				BREAK_NOP;	// for debugging
 			if (!value->visit_facts(inputs, param_cg_context)) { 
 				return false;
 			}
@@ -497,7 +498,7 @@ FunctionInvocation::visit_facts(vector<const Fact*>& inputs, CGContext& cg_conte
 			// when we generate subsequent parameters within this invocation.
 			running_eff_context.add_effect(param_eff_accum);
 			// Update the total effect of this invocation, too.
-			cg_context.add_effect(param_eff_accum);  
+			cg_context.add_effect(param_eff_accum); 
 		}
 		ok = true;
 	} 
diff --git a/src/FunctionInvocationBinary.cpp b/src/FunctionInvocationBinary.cpp
index 6cc81262e..b4c98a170 100644
--- a/src/FunctionInvocationBinary.cpp
+++ b/src/FunctionInvocationBinary.cpp
@@ -243,6 +243,8 @@ FunctionInvocationBinary::get_type(void) const
 		}
 		break;
 	}
+	assert(0);
+	return Type::get_simple_type(eInt);
 }
 
 ///////////////////////////////////////////////////////////////////////////////
diff --git a/src/FunctionInvocationUnary.cpp b/src/FunctionInvocationUnary.cpp
index c1f91462d..4cf26b590 100644
--- a/src/FunctionInvocationUnary.cpp
+++ b/src/FunctionInvocationUnary.cpp
@@ -136,6 +136,8 @@ FunctionInvocationUnary::get_type(void) const
 		return Type::get_simple_type(eInt);
 		break;
 	}
+	assert(0);
+	return Type::get_simple_type(eInt);
 }
 
 /*
diff --git a/src/FunctionInvocationUser.cpp b/src/FunctionInvocationUser.cpp
index 59fefd704..2ac477ee4 100644
--- a/src/FunctionInvocationUser.cpp
+++ b/src/FunctionInvocationUser.cpp
@@ -70,15 +70,14 @@ static vector<const FunctionInvocationUser*> invocations;   // list of function
 static vector<const Fact*> return_facts;              // list of return facts
 
 const Fact*
-get_return_fact_for_invocation(const FunctionInvocationUser* fiu, enum eFactCategory cat) 
+get_return_fact_for_invocation(const FunctionInvocationUser* fiu, const Variable* var, enum eFactCategory cat) 
 {
 	assert(invocations.size() == return_facts.size());
 	for (size_t i=0; i<return_facts.size(); i++) {
-		if (return_facts[i]->eCat == cat) {
-			if (invocations[i] == fiu) {
-				const Variable* v = return_facts[i]->get_var();
-				assert(v == fiu->get_func()->rv);
-				return return_facts[i];
+		if (invocations[i] == fiu) {
+			const Fact* fact = return_facts[i];
+			if (fact->eCat == cat && fact->get_var() == var) { 
+				return fact;
 			}
 		}
 	}
@@ -91,7 +90,7 @@ add_return_fact_for_invocation(const FunctionInvocationUser* fiu, const Fact* f)
 	size_t i;
 	assert(invocations.size() == return_facts.size());
 	for (i=0; i<invocations.size(); i++) {
-		if (invocations[i] == fiu) {
+		if (invocations[i] == fiu && return_facts[i]->is_related(*f)) {
 			return_facts[i] = f;
 			return;
 		}
@@ -186,6 +185,8 @@ FunctionInvocationUser::build_invocation_and_function(CGContext &cg_context, con
 	Effect running_eff_context(cg_context.get_effect_context()); 
 	Function* func = Function::make_random_signature(cg_context, type, qfer);
 
+	if (func->name == "func_51")
+		BREAK_NOP;		// for debugging
 	vector<const Expression*> param_values;
 	size_t i;
 	for (i = 0; i < func->param.size(); i++) { 
@@ -254,9 +255,9 @@ FunctionInvocationUser::build_invocation(Function *target, CGContext &cg_context
 	Effect running_eff_context(cg_context.get_effect_context()); 
 	FactMgr* fm = get_fact_mgr(&cg_context);
 	// XXX DEBUGGING
-	// if (func->name == "func_43" && cg_context.get_current_func()->name=="func_1") {
-	// 	i = 0; // Set breakpoint here.
-	// }
+	if (func->name == "func_10" && cg_context.get_current_func()->name=="func_1") {
+	 	i = 0; // Set breakpoint here.
+	}
 
 	for (i = 0; i < func->param.size(); i++) { 
 		Effect param_eff_accum;  
@@ -315,7 +316,7 @@ FunctionInvocationUser::revisit(std::vector<const Fact*>& inputs, CGContext& cg_
 		fm->setup_in_out_maps(true);
 	}
 	// for debugging
-	if (func->name=="func_8" && func->visited_cnt==2) {
+	if (func->name=="func_10" && func->visited_cnt==19) {
 		//cout << func->visited_cnt << endl;
 		//func->Output(cout);
 		//cout << endl;
@@ -368,7 +369,7 @@ FunctionInvocationUser::save_return_fact(const vector<const Fact*>& facts) const
 {
 	size_t i;
 	for (i=0; i<facts.size(); i++) {
-		if (facts[i]->get_var() == func->rv) {
+		if (func->rv->match(facts[i]->get_var())) {
 			add_return_fact_for_invocation(this, facts[i]);
 		}
 	}
diff --git a/src/FunctionInvocationUser.h b/src/FunctionInvocationUser.h
index 8c682cacf..1879d4813 100644
--- a/src/FunctionInvocationUser.h
+++ b/src/FunctionInvocationUser.h
@@ -99,7 +99,7 @@ class FunctionInvocationUser: public FunctionInvocation
 	bool build_invocation(Function *target, CGContext &cg_context);
 };
 
-const Fact* get_return_fact_for_invocation(const FunctionInvocationUser* fiu, enum eFactCategory cat);
+const Fact* get_return_fact_for_invocation(const FunctionInvocationUser* fiu, const Variable* var, enum eFactCategory cat);
 
 void calls_to_funcs(const vector<const FunctionInvocationUser*>& calls, vector<const Function*>& funcs);
 void calls_to_funcs_recursive(const vector<const FunctionInvocationUser*>& calls, vector<const Function*>& funcs);
diff --git a/src/ProbabilityTable.h b/src/ProbabilityTable.h
index 2707af730..56ee97e80 100644
--- a/src/ProbabilityTable.h
+++ b/src/ProbabilityTable.h
@@ -33,6 +33,7 @@
 #include <vector>
 #include <algorithm>
 #include <functional>
+#include <assert.h>
 #include "Probabilities.h"
 #include "VectorFilter.h"
 #include "CGOptions.h"
@@ -41,11 +42,9 @@
 using namespace std;
 
 template <class Key, class Value>
-class Table {
+class TableEntry {
 public:
-	Table(Key k, Value v);
-
-	~Table();
+	TableEntry(Key k, Value v);
 
 	Key get_key() { return key_; }
 
@@ -53,13 +52,12 @@ class Table {
 
 private:
 	Key key_;
-
 	Value value_;
 };
 
 template <class Key, class Value>
 class ProbabilityTable {
-	typedef Table<Key, Value> Tbl;
+	typedef TableEntry<Key, Value> Entry;
 
 public:
 	ProbabilityTable();
@@ -70,41 +68,25 @@ class ProbabilityTable {
 
 	void add_elem(Key k, Value v);
 
-	void sorted_insert(Tbl *t);
+	void sorted_insert(Entry *t);
 
 	Value get_value(Key k);
 
-	Filter *get_filter() { return vf_; }
-
-	bool filter(Key k);
 private:
 	Key curr_max_key_;
-
-	std::vector<Tbl *> table_;
-
-	VectorFilter *vf_;
-
-	std::vector<Key> vs_;
+	std::vector<Entry *> table_; 
 };
 
 template <class Key, class Value>
-Table<Key, Value>::Table(Key k, Value v)
+TableEntry<Key, Value>::TableEntry(Key k, Value v)
 	: key_(k),
 	  value_(v)
 {
-
-}
-
-template <class Key, class Value>
-Table<Key, Value>::~Table()
-{
-
 }
 
 template <class Key, class Value>
 ProbabilityTable<Key, Value>::ProbabilityTable()
-	: curr_max_key_(0),
-          vf_(NULL)
+	: curr_max_key_(0)
 {
 	table_.clear();
 }
@@ -112,7 +94,7 @@ ProbabilityTable<Key, Value>::ProbabilityTable()
 template <class Key, class Value>
 ProbabilityTable<Key, Value>::~ProbabilityTable()
 {
-	typename vector<Tbl *>::iterator i;
+	typename vector<Entry *>::iterator i;
 	for (i = table_.begin(); i != table_.end(); ++i) 
 		delete (*i);
 	table_.clear();
@@ -126,14 +108,14 @@ void ProbabilityTable<Key, Value>::initialize(ProbName pname)
 }
 
 template <class Key, class Value>
-bool my_less(Table<Key, Value> *t, Key k2)
+bool my_less(TableEntry<Key, Value> *t, Key k2)
 {
 	Key k1 = t->get_key();
 	return (k1 < k2);
 }
 
 template <class Key, class Value>
-bool my_greater(Table<Key, Value> *t, Key k2)
+bool my_greater(TableEntry<Key, Value> *t, Key k2)
 {
 	Key k1 = t->get_key();
 	return (k1 > k2);
@@ -141,7 +123,7 @@ bool my_greater(Table<Key, Value> *t, Key k2)
 
 template <class Key, class Value>
 void
-ProbabilityTable<Key, Value>::sorted_insert(Tbl *t)
+ProbabilityTable<Key, Value>::sorted_insert(Entry *t)
 {
 	assert(t);
 	
@@ -153,7 +135,7 @@ ProbabilityTable<Key, Value>::sorted_insert(Tbl *t)
 		return;
 	}
 	
-	typename vector<Tbl *>::iterator i;
+	typename vector<Entry *>::iterator i;
 	for (i=table_.begin(); i!=table_.end(); i++) {
 		if (my_greater<Key, Value>(*i, k)) {
 			break;
@@ -174,7 +156,7 @@ template <class Key, class Value>
 void
 ProbabilityTable<Key, Value>::add_elem(Key k, Value v)
 {
-	Tbl *t = new Tbl(k, v);
+	Entry *t = new Entry(k, v);
 	sorted_insert(t);
 }
 
@@ -184,30 +166,11 @@ ProbabilityTable<Key, Value>::get_value(Key k)
 {
 	assert(k < curr_max_key_);
 
-	typename vector<Tbl *>::iterator i;
+	typename vector<Entry *>::iterator i;
 	i = find_if(table_.begin(), table_.end(), std::bind2nd(std::ptr_fun(my_greater<Key, Value>), k));
 
 	assert(i != table_.end());
 	return (*i)->get_value();
 }
 
-template <class Key, class Value>
-bool
-ProbabilityTable<Key, Value>::filter(Key k)
-{
-	assert(k < curr_max_key_);
-	if (vf_ == NULL) {
-		typename vector<Tbl *>::iterator i;
-		for (i = table_.begin(); i != table_.end(); ++i) {
-			Key tmp_k = (*i)->get_key();
-			assert(tmp_k > 0);
-			vs_.push_back(tmp_k-1);
-		}
-		vf_ = new VectorFilter(vs_, NOT_FILTER_OUT);
-	}
-
-	vf_->disable(fDefault);
-	return vf_->filter(k);
-}
-
 #endif
diff --git a/src/Statement.cpp b/src/Statement.cpp
index 45a23187e..b88066c26 100644
--- a/src/Statement.cpp
+++ b/src/Statement.cpp
@@ -138,9 +138,6 @@ bool StatementFilter::filter(int value) const
 	if (!this->valid_filter())
 		return false;
 
-	if (Statement::stmtTable_->filter(value))
-		return true;
-
 	eStatementType type = Statement::number_to_type(value);
 
 	// If expand_check returns false, we filter out v. 
@@ -890,13 +887,13 @@ Statement::post_creation_analysis(vector<const Fact*>& pre_facts, const Effect&
 			FactVec outputs = pre_facts;
 			cg_context.reset_effect_accum(pre_effect); 
 			//if (stm_id == 573)
-			//	BREAK_NOP;
-			if (!validate_and_update_facts(outputs, cg_context)) { 
 				/*if (this->eType == eAssign) {
 					((const StatementAssign*)this)->get_rhs()->indented_output(cout, 0);
 				}
 				cout << endl;
 				Output(cout, fm);*/
+			}
+			if (!validate_and_update_facts(outputs, cg_context)) {
 				assert(0);
 			}
 			fm->global_facts = outputs;
diff --git a/src/StatementAssign.cpp b/src/StatementAssign.cpp
index 60f0f8523..f56cfce46 100644
--- a/src/StatementAssign.cpp
+++ b/src/StatementAssign.cpp
@@ -85,7 +85,7 @@ bool
 StatementAssignFilter::filter(int v) const
 {
 	assert(table_);
-	return table_->filter(v);
+	return false;
 }
 
 //////////////////////////////////////////////////////////////////////////////
@@ -132,29 +132,38 @@ AssignOpsProbability(Filter *filter = NULL)
  *
  */
 StatementAssign *
-StatementAssign::make_random(CGContext &cg_context)
+StatementAssign::make_random(CGContext &cg_context, const Type* type, const CVQualifiers* qf)
 {
-	DEPTH_GUARD_BY_TYPE_RETURN(dtStatementAssign, NULL);
-	StatementAssign::InitProbabilityTable();
-	StatementAssignFilter filter(StatementAssign::assignOpsTable_);
-	eAssignOps op = AssignOpsProbability(&filter);
-	ERROR_GUARD(NULL);
-
+	// decide assignment operator
+	eAssignOps op;
+	if (type && type->eType != eSimple) {
+		op = eSimpleAssign;
+	} else {
+		DEPTH_GUARD_BY_TYPE_RETURN(dtStatementAssign, NULL);
+		StatementAssign::InitProbabilityTable();
+		StatementAssignFilter filter(StatementAssign::assignOpsTable_);
+		op = AssignOpsProbability(&filter);
+		ERROR_GUARD(NULL);
+	}
+	// decide type
+	if (type == NULL) {
+		type = Type::SelectLType(!cg_context.get_effect_context().is_side_effect_free(), op);
+	}
+	assert(!type->is_const_struct_union());
+	
 	FactMgr* fm = get_fact_mgr(&cg_context);
 	assert(fm);
+	fm->backup_facts();
 
-	Lhs *lhs = 0;
+	// pre-generation initializations
+	Lhs *lhs = NULL;
 	Expression *e = NULL;
-	fm->backup_facts();
-  
-	const Type* t = Type::SelectLType(!cg_context.get_effect_context().is_side_effect_free(), op);
-	ERROR_GUARD(NULL);
 	cg_context.expr_depth = 0;
-	
 	Effect running_eff_context(cg_context.get_effect_context());
 	Effect rhs_accum, lhs_accum;  
 	CGContext rhs_cg_context(cg_context, running_eff_context, &rhs_accum);
-	e = Expression::make_random(rhs_cg_context, t);
+	
+	e = Expression::make_random(rhs_cg_context, type, qf);
 	ERROR_GUARD_AND_DEL1(NULL, e);
 	CVQualifiers qfer = e->get_qualifiers();
 	// lhs should not has "const" qualifier
@@ -169,7 +178,7 @@ StatementAssign::make_random(CGContext &cg_context)
 	cg_context.add_effect(rhs_accum);
 	CGContext lhs_cg_context(cg_context, running_eff_context, &lhs_accum);
 	lhs_cg_context.get_effect_stm() = rhs_cg_context.get_effect_stm();
-	lhs = Lhs::make_random(lhs_cg_context, t, &qfer);
+	lhs = Lhs::make_random(lhs_cg_context, type, &qfer);
 	ERROR_GUARD_AND_DEL2(NULL, e, lhs);
 
 	// Yang: Is it a bug?
@@ -183,7 +192,7 @@ StatementAssign::make_random(CGContext &cg_context)
 	}
 
 	cg_context.add_effect(lhs_accum);
-	cg_context.get_effect_stm() = lhs_cg_context.get_effect_stm();
+	//cg_context.get_effect_stm() = cg_context.get_effect_stm();
 	
 	// book keeping
 	incr_counter(Bookkeeper::expr_depth_cnts, cg_context.expr_depth);
@@ -319,7 +328,7 @@ StatementAssign::visit_facts(vector<const Fact*>& inputs, CGContext& cg_context)
 		return false;
 	}
 	cg_context.add_effect(lhs_accum);
-	cg_context.get_effect_stm() = lhs_cg_context.get_effect_stm();
+	//cg_context.get_effect_stm() = lhs_cg_context.get_effect_stm();
 	update_fact_for_assign(this, inputs);
 	// save effect
 	FactMgr* fm = get_fact_mgr(&cg_context);
@@ -396,7 +405,7 @@ StatementAssign::StatementAssign(const StatementAssign &sa)
  *
  */
 StatementAssign::~StatementAssign(void)
-{ 
+{
 	if (rhs != &expr) {
 		delete rhs;
 	}
diff --git a/src/StatementAssign.h b/src/StatementAssign.h
index 8d0652d77..1b141b161 100644
--- a/src/StatementAssign.h
+++ b/src/StatementAssign.h
@@ -80,7 +80,7 @@ class StatementAssign : public Statement
 {
 public:
 	// Factory method.
-	static StatementAssign *make_random(CGContext &cg_context);
+	static StatementAssign *make_random(CGContext &cg_context, const Type* type=0, const CVQualifiers* qfer=0);
 
 	static StatementAssign *make_possible_compound_assign(CGContext &cg_context,
 						 const Lhs &l,
diff --git a/src/StatementBreak.cpp b/src/StatementBreak.cpp
index ce22c686c..ca0072e79 100644
--- a/src/StatementBreak.cpp
+++ b/src/StatementBreak.cpp
@@ -70,7 +70,7 @@ StatementBreak::make_random(CGContext &cg_context)
 	}
 	assert(b);
 	cg_context.get_effect_stm().clear();
-	Expression *expr = Expression::make_random(cg_context, get_int_type(), true, true, eVariable);
+	Expression *expr = Expression::make_random(cg_context, get_int_type(), 0, true, true, eVariable);
 	ERROR_GUARD(NULL);    
 	StatementBreak* sc = new StatementBreak(cg_context.get_current_block(), *expr, *b); 
 	b->break_stms.push_back(sc);
diff --git a/src/StatementContinue.cpp b/src/StatementContinue.cpp
index e106f3482..aad41ae63 100644
--- a/src/StatementContinue.cpp
+++ b/src/StatementContinue.cpp
@@ -70,7 +70,7 @@ StatementContinue::make_random(CGContext &cg_context)
 	}
 	assert(b);
 	cg_context.get_effect_stm().clear();
-	Expression *expr = Expression::make_random(cg_context, get_int_type(), true, true, eVariable);
+	Expression *expr = Expression::make_random(cg_context, get_int_type(), 0, true, true, eVariable);
 	ERROR_GUARD(NULL); 
 	StatementContinue* sc = new StatementContinue(cg_context.get_current_block(), *expr, *b); 
 	fm->create_cfg_edge(sc, b, false, true);  
diff --git a/src/StatementFor.cpp b/src/StatementFor.cpp
index 6b0d8f398..29406df4b 100644
--- a/src/StatementFor.cpp
+++ b/src/StatementFor.cpp
@@ -146,7 +146,11 @@ StatementFor::make_iteration(CGContext& cg_context, StatementAssign*& init, Expr
 	do {
 		var = VariableSelector::SelectLoopCtrlVar(cg_context, invalid_vars); 
 		ERROR_GUARD(NULL);
-		if (var->is_volatile()) {
+		if (var->is_volatile() || 
+			// disallow an integer field of an union, which also has a pointer field, to be IV because
+			// increment IV would cause the pointer to be invalid, and the current points-to analysis
+			// simply assumes loop stepping has no pointer effect
+			(var->is_inside_union_field() && var->get_top_container()->type->contain_pointer_field()) ) {
 			invalid_vars.push_back(var);
 		} else {
 			break;
diff --git a/src/StatementIf.cpp b/src/StatementIf.cpp
index 1b9ce5294..6b17427ad 100644
--- a/src/StatementIf.cpp
+++ b/src/StatementIf.cpp
@@ -66,7 +66,7 @@ StatementIf::make_random(CGContext &cg_context)
 		pre_facts = fm->global_facts;
 	}
 	cg_context.get_effect_stm().clear();
-	Expression *expr = Expression::make_random(cg_context, get_int_type(), false, !CGOptions::const_as_condition());
+	Expression *expr = Expression::make_random(cg_context, get_int_type(), NULL, false, !CGOptions::const_as_condition());
 	ERROR_GUARD(NULL);
 	// func_1 hacking, re-analyze for multiple function calls
 	if (cg_context.get_current_func()->name == "func_1" && !(cg_context.flags & IN_LOOP)) {
diff --git a/src/Type.cpp b/src/Type.cpp
index 38acd3e43..261f3b12c 100644
--- a/src/Type.cpp
+++ b/src/Type.cpp
@@ -1396,7 +1396,7 @@ Type::SizeInBytes(void) const
 			unsigned int sz = 0;
 			if (is_bitfield(i)) {
 				assert(i < bitfields_length_.size());
-				sz = ceil(bitfields_length_[i] / 8.0) * 8;
+				sz = (int)(ceil(bitfields_length_[i] / 8.0) * 8);
 			} else {
 				sz = fields[i]->SizeInBytes();
 			}
@@ -1418,7 +1418,7 @@ Type::SizeInBytes(void) const
         }
         return total_size;
     }
-	case ePointer: return CGOptions::x86_64() ? 8 : 4; 
+	case ePointer: return 8; //CGOptions::x86_64() ? 8 : 4; 
 	}
 	return 0;
 }
@@ -1474,12 +1474,10 @@ Type::get_int_subfield_names(string prefix, vector<string>& names, const vector<
 		size_t i;
 		size_t j = 0;
 		for (i=0; i<fields.size(); i++) {
-			// skip 0 length bitfields
-			if (is_unamed_padding(i)) {
-				continue;
-			}
-			if (std::find(excluded_fields.begin(), excluded_fields.end(), i) != excluded_fields.end()) {
-				j++;
+			// skip 0 length bitfields and excluded fields
+			if (std::find(excluded_fields.begin(), excluded_fields.end(), i) != excluded_fields.end() ||
+				is_unamed_padding(i)) {
+				if (!is_unamed_padding(i)) j++;
 				continue;
 			}
 			ostringstream oss;
@@ -1490,6 +1488,20 @@ Type::get_int_subfield_names(string prefix, vector<string>& names, const vector<
 	}
 }
 
+bool 
+Type::contain_pointer_field(void) const
+{
+	if (eType == ePointer) return true;
+	if (eType == eStruct || eType == eUnion) {
+		for (size_t i=0; i<fields.size(); i++) {
+			if (fields[i]->contain_pointer_field()) {
+				return true;
+			}
+		}
+	}
+	return false;
+}
+
 // ---------------------------------------------------------------------
 void
 Type::Output(std::ostream &out) const
diff --git a/src/Type.h b/src/Type.h
index a55d43342..5e4eeca7b 100644
--- a/src/Type.h
+++ b/src/Type.h
@@ -225,6 +225,7 @@ class Type
 	bool is_full_bitfields_struct() const;
 	bool is_bitfield(size_t index) const ;
 	bool has_bitfields() const;
+	bool contain_pointer_field(void) const;
 	bool is_const_struct_union() const;
 	bool is_volatile_struct_union() const;
 	bool is_int(void) const { return eType == eSimple && simple_type != eVoid;}
diff --git a/src/Variable.cpp b/src/Variable.cpp
index 595b7071d..9529c0e64 100644
--- a/src/Variable.cpp
+++ b/src/Variable.cpp
@@ -287,6 +287,14 @@ bool Variable::has_field_var(const Variable* v) const
     return false;
 }
 
+const Variable* 
+Variable::get_top_container(void) const
+{
+	const Variable* v = this;
+	for (; v && v->field_var_of; v = v->field_var_of);
+	return v;
+}
+
 int  
 Variable::get_field_id(void) const
 { 
@@ -309,7 +317,7 @@ void Variable::create_field_vars(const Type *type)
     size_t i, j;
     assert(type->fields.size() == type->qfers_.size());
 	j = 0;
-	if (name == "g_371")
+	if (name == "g_481")
 		j = 0;
     bool is_vol_var = qfer.is_volatile();
     bool is_const_var = qfer.is_const();
@@ -358,7 +366,9 @@ Variable::CreateVariable(const std::string &name, const Type *type,
 	if (type->eType == eSimple)
 		assert(type->simple_type != eVoid);
 
-	var->init = Constant::make_random(type);
+	const Variable* top = isFieldVarOf;
+	while (top->field_var_of) top = top->field_var_of;
+	var->init = (top->type->eType == eUnion) ? 0 : Constant::make_random(type);
 
 	ERROR_GUARD_AND_DEL1(NULL, var);
 	if (type->is_aggregate()) {
@@ -447,6 +457,12 @@ Variable::is_global(void) const
 	return (name.find("g_") == 0);
 }
 
+bool
+Variable::is_local(void) const
+{
+	return (name.find("l_") == 0);
+}
+
 // ------------------------------------------------------------- 
 bool
 Variable::is_visible_local(const Block* blk) const
@@ -1330,7 +1346,20 @@ Variable::compare_field(const Variable* v) const
 	}
 	return 0;
 }
-	 
+
+void 
+Variable::find_pointer_fields(vector<const Variable*>& ptr_fields) const
+{
+	for (size_t i=0; i<field_vars.size(); i++) {
+		if (field_vars[i]->is_pointer()) {
+			ptr_fields.push_back(field_vars[i]);
+		}
+		else if (field_vars[i]->is_aggregate()) {
+			field_vars[i]->find_pointer_fields(ptr_fields);
+		}
+	}
+}
+
 ///////////////////////////////////////////////////////////////////////////////
 
 // Local Variables:
diff --git a/src/Variable.h b/src/Variable.h
index 601c634b2..bd11b7602 100644
--- a/src/Variable.h
+++ b/src/Variable.h
@@ -77,6 +77,7 @@ class Variable
 
 	virtual ~Variable(void);
 	virtual bool is_global(void) const; 
+	virtual bool is_local(void) const;
 	virtual bool is_visible_local(const Block* blk) const;
 	virtual size_t get_dimension(void) const { return 0;}
 	bool is_visible(const Block* blk) const { return is_global() || is_visible_local(blk);}
@@ -88,17 +89,20 @@ class Variable
 	bool is_volatile_after_deref(int deref_level) const;
 	bool has_field_var(const Variable* v) const; 
 	bool is_field_var(void) const { return field_var_of != 0; };
+	const Variable* get_top_container(void) const;
 	int  get_field_id(void) const;
 	bool is_union_field(void) const { return field_var_of != 0 && field_var_of->type->eType == eUnion; };
+	bool is_inside_union_field(void) const { return is_union_field() || (field_var_of && field_var_of->is_union_field()); }
 	bool is_array_field(void) const;
 	bool is_virtual(void) const;
 	bool is_aggregate(void) const { return type && type->is_aggregate(); }
 	bool match(const Variable* v) const;
 	bool loose_match(const Variable* v) const;
 	bool is_pointer(void) const { return type && type->eType == ePointer;}
-	bool is_rv(void) const { return StringUtils::end_with(name, "_rv"); }
+	bool is_rv(void) const { return name.find("_rv") != string::npos; }
 	int  compare_field(const Variable* v) const;
 	int get_seq_num(void) const;
+	void find_pointer_fields(vector<const Variable*>& ptr_fields) const;
 
 	virtual std::string get_actual_name() const;
 	std::string to_string(void) const;
diff --git a/src/VariableSelector.cpp b/src/VariableSelector.cpp
index ae61ef425..1e020ca22 100644
--- a/src/VariableSelector.cpp
+++ b/src/VariableSelector.cpp
@@ -101,9 +101,6 @@ VariableSelectFilter::~VariableSelectFilter()
 bool
 VariableSelectFilter::filter(int v) const
 {
-	if (VariableSelector::scopeTable_->filter(v))
-		return true;
-
 	eVariableScope scope = VariableSelector::scopeTable_->get_value(v);
 	if (scope == eParentParam) {
 		Function &parent = *cg_context_.get_current_func();
@@ -227,9 +224,9 @@ bool
 VariableSelector::is_eligible_var(const Variable* var, int deref_level, Effect::Access access, const CGContext& cg_context)
 {
 	const Variable* coll = var->get_collective();
+	FactMgr* fm = get_fact_mgr(&cg_context);
 	if (coll != var) {
 		CGContext cg_tmp(cg_context);
-		FactMgr* fm = get_fact_mgr(&cg_context);
 		if (!cg_tmp.read_indices(var, fm->global_facts)) {
 			return false;
 		}
@@ -274,7 +271,9 @@ VariableSelector::is_eligible_var(const Variable* var, int deref_level, Effect::
 	//
 	// We cannot read a variable if the current code-generation context
 	// says that we should not.
-	if ((access == Effect::READ) && cg_context.is_nonreadable(var)) {
+	if ((access == Effect::READ) && 
+		(cg_context.is_nonreadable(var) ||
+		(FactUnion::is_nonreadable_field(var, fm->global_facts)))) {
 		return false;
 	}
 	// ISSUE: generating "interesting" C programs.
@@ -1439,14 +1438,6 @@ VariableSelector::create_mutated_array_var(const ArrayVariable* av, const vector
 	return new_av;
 }
 
-Variable *
-VariableSelector::make_dummy_variable(const string &name, const Type* t, const CVQualifiers* qfer)
-{
-	Variable *var = new Variable(name, t, 0, qfer);
-	AllVars.push_back(var);
-	return var;
-}
-
 Variable *
 VariableSelector::make_dummy_static_variable(const string &name)
 {
diff --git a/src/VariableSelector.h b/src/VariableSelector.h
index 6a479d9fa..94828853d 100644
--- a/src/VariableSelector.h
+++ b/src/VariableSelector.h
@@ -62,7 +62,6 @@ class VariableSelector
 public:
 	VariableSelector(void) {};
 	static Variable* new_variable(const std::string &name, const Type *type, const Expression* init, const CVQualifiers* qfer);
-	static Variable *make_dummy_variable(const string &name, const Type* t, const CVQualifiers* qfer);
 	// ISSUE: use it only when you want to create a static variable
 	static Variable *make_dummy_static_variable(const string &name);
 	
diff --git a/src/VectorFilter.cpp b/src/VectorFilter.cpp
index c1726793f..f92c0fcaf 100644
--- a/src/VectorFilter.cpp
+++ b/src/VectorFilter.cpp
@@ -35,13 +35,22 @@
 using namespace std;
 
 VectorFilter::VectorFilter(void) 
-	:  flag_(FILTER_OUT) 
+	: ptable(NULL), 
+	  flag_(FILTER_OUT) 
+{
+	//Nothing to do
+}
+
+VectorFilter::VectorFilter(ProbabilityTable<unsigned int, int> *table) 
+	: ptable(table), 
+	  flag_(FILTER_OUT) 
 {
 	//Nothing to do
 }
 
 VectorFilter::VectorFilter(std::vector<unsigned int> &vs, int flag) 
 	: vs_(vs),
+	  ptable(NULL),
 	  flag_(flag) 
 {
 	//Nothing to do
@@ -58,6 +67,17 @@ VectorFilter::filter(int v) const
 	if (!this->valid_filter())
 		return false;
 
+	if (ptable) {
+		v = ptable->get_value(v);
+	}
 	bool re = std::find(vs_.begin(), vs_.end(), static_cast<unsigned int>(v)) != vs_.end();
 	return (flag_ == FILTER_OUT) ? re : !re;
+}
+
+int
+VectorFilter::lookup(int v) const
+{
+	if (!this->valid_filter() || ptable == NULL)
+		return v; 
+	return v = ptable->get_value(v);
 }
\ No newline at end of file
diff --git a/src/VectorFilter.h b/src/VectorFilter.h
index 81fb252ce..2a056353e 100644
--- a/src/VectorFilter.h
+++ b/src/VectorFilter.h
@@ -32,6 +32,7 @@
 
 #include <vector>
 #include "Filter.h"
+#include "ProbabilityTable.h"
 
 // Filter out elements from the vector, i.e., elements in the vector
 // is invalid.
@@ -43,16 +44,21 @@ class VectorFilter : public Filter
 {
 public:
 	VectorFilter(void);
+	VectorFilter(ProbabilityTable<unsigned int, int> *table);
 	explicit VectorFilter(std::vector<unsigned int> &vs, int flag = FILTER_OUT);
 
 	VectorFilter& add(unsigned int item) { vs_.push_back(item); return *this;}
 
+	int lookup(int v) const;
+
 	virtual ~VectorFilter(void);
 
 	virtual bool filter(int v) const;
 private:
 	std::vector<unsigned int> vs_;
 
+	ProbabilityTable<unsigned int, int> *ptable;
+
 	int flag_;
 };