fix to Corral to instrument user defined types such as ref

AddOns/AngelicVerifierNull/test/propinst-regressions/rodrigo_refnull.bpl

@@ -0,0 +1,9 @@
+type Ref;
+
+const unique null : Ref;
+var r: Ref;
+
+procedure Foo() {
+ r := null;
+ assume {:nonnull} r != null;
+}

AddOns/PropInst/PropInst/ExampleProperties/nullcheck-csharp.avp

@@ -0,0 +1,21 @@
+GlobalDeclarations
+{
+function {:inline} {:aliasingQuery} {:mkUniqueFn} aliasQ(p:Ref, q:Ref) returns (bool) { p == q }
+}
+
+
+TemplateVariables
+{
+var p : Ref;
+}
+
+
+//Check every dereference
+CmdRule
+{
+ assume {:nonnull} p != null;
+}
+-->
+{
+ assert p != null;
+}