diff --git a/AddOns/AngelicVerifierNull/test/propinst-regressions/Answer b/AddOns/AngelicVerifierNull/test/propinst-regressions/Answer
index a5b969f2c..8b1534caa 100644
--- a/AddOns/AngelicVerifierNull/test/propinst-regressions/Answer
+++ b/AddOns/AngelicVerifierNull/test/propinst-regressions/Answer
@@ -1,50 +1,55 @@
-
--------------------- uaf0.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing uaf0_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
-
--------------------- uaf1.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing uaf1_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
-
--------------------- df0.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing df0_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
-
--------------------- uaf2.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing uaf2_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])
-
--------------------- uaf3.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing uaf3_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])
-
--------------------- irql0.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing irql0_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 2)
-
--------------------- irql1.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing irql1_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 1)
-
--------------------- irql2.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing irql2_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int, x_2: int :: unknownTrigger_0(x_1) && unknownTrigger_1(x_2) ==> x_1 <= x_2)
-
--------------------- null0.bpl --------------------
-[TAG: AV_OUTPUT] ----- Analyzing null0_pinst_hinst.bpl ------
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace0 }
-[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr !(ax == NULL)
+
+-------------------- uaf0.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing uaf0_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
+
+-------------------- uaf1.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing uaf1_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
+
+-------------------- df0.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing df0_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
+
+-------------------- uaf2.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing uaf2_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])
+
+-------------------- uaf3.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing uaf3_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1])
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace1 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr validFree[p] || p == 0
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_3(x_1) ==> validFree[x_1 + 1])
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_2: int :: unknownTrigger_1(x_2) ==> validFree[x_2])
+
+-------------------- irql0.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing irql0_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 2)
+
+-------------------- irql1.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing irql1_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int :: unknownTrigger_0(x_1) ==> x_1 <= 1)
+
+-------------------- irql2.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing irql2_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] EXPLAINERROR-BLOCK :: (forall x_1: int, x_2: int :: unknownTrigger_0(x_1) && unknownTrigger_1(x_2) ==> x_1 <= x_2)
+
+-------------------- null0.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing null0_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace0 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc foo with expr !(ax == NULL)
+
+-------------------- rodrigo_refnull.bpl --------------------
+[TAG: AV_OUTPUT] ----- Analyzing rodrigo_refnull_pinst_hinst.bpl ------
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Failing traces {Trace0 }
+[TAG: AV_OUTPUT] ANGELIC_VERIFIER_WARNING: Assertion failed in proc Foo with expr r != null
diff --git a/AddOns/AngelicVerifierNull/test/propinst-regressions/runtest.bat b/AddOns/AngelicVerifierNull/test/propinst-regressions/runtest.bat
index f26e4e131..229c1d06c 100644
--- a/AddOns/AngelicVerifierNull/test/propinst-regressions/runtest.bat
+++ b/AddOns/AngelicVerifierNull/test/propinst-regressions/runtest.bat
@@ -18,6 +18,7 @@ call:add irql0.bpl ..\..\..\PropInst\PropInst\ExampleProperties\checkIrql-razzle
 call:add irql1.bpl ..\..\..\PropInst\PropInst\ExampleProperties\checkIrql-razzle.avp
 call:add irql2.bpl ..\..\..\PropInst\PropInst\ExampleProperties\checkIrql-razzle.avp
 call:add null0.bpl ..\..\..\PropInst\PropInst\ExampleProperties\nullcheck-razzle.avp
+call:add rodrigo_refnull.bpl ..\..\..\PropInst\PropInst\ExampleProperties\nullcheck-csharp.avp
 
 REM for %%f in (eeSlice3.bpl) do (
 set i=0
diff --git a/source/Util/Visitor.cs b/source/Util/Visitor.cs
index 025f128fd..059f4ef59 100644
--- a/source/Util/Visitor.cs
+++ b/source/Util/Visitor.cs
@@ -1294,7 +1294,7 @@ public override Expr VisitNAryExpr(NAryExpr node)
                 var nodeFunc = ((FunctionCall)node.Fun).Func;
                 for (var i = 0; i < tcFunc.InParams.Count; i++)
                 {
-                    if (!Equals(tcFunc.InParams[i].TypedIdent.Type, nodeFunc.InParams[i].TypedIdent.Type))
+                    if (!Equals(tcFunc.InParams[i].TypedIdent.Type.ToString(), nodeFunc.InParams[i].TypedIdent.Type.ToString()))
                     {
                         Matches = false;
                         return base.VisitNAryExpr(node);
@@ -1355,7 +1355,7 @@ public override Expr VisitIdentifierExpr(IdentifierExpr node)
 
             if (idexToConsume.Decl != null)
             {
-                if (Equals(node.Decl.TypedIdent.Type, idexToConsume.Decl.TypedIdent.Type)
+                if (Equals(node.Decl.TypedIdent.Type.ToString(), idexToConsume.Decl.TypedIdent.Type.ToString())
                     && AreAttributesASubset(idexToConsume.Decl.Attributes, node.Decl.Attributes))
                 {
                     Substitution.Add(idexToConsume.Decl, node);