Fix type solving procedure

Author: sergeypospelov

usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt

@@ -307,9 +307,14 @@ class UTypeConstraints<Type>(
                     var nextRegion = currentRegion.intersect(region) // add [heapRef] to the current region
                     if (nextRegion.isEmpty) {
                         // conflict detected, so it's impossible for [potentialConflictingRefs]
-                        // to have the common type with [heapRef], therefore they can't be equal
-                        val disjunct = potentialConflictingRefs.map {
-                            with(it.ctx) { it.neq(heapRef) }
+                        // to have the common type with [heapRef], therefore they can't be equal or
+                        // some of them equals null
+                        val disjunct = mutableListOf<UBoolExpr>()
+                        potentialConflictingRefs.mapTo(disjunct) { ref ->
+                            with(ref.uctx) { ref.neq(heapRef) }
+                        }
+                        potentialConflictingRefs.mapTo(disjunct) { ref ->
+                            with(ref.uctx) { ref.eq(nullRef) }
                         }
                         bannedRefEqualities += heapRef.ctx.mkOr(disjunct)
 

usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt

@@ -180,8 +180,8 @@ class TypeSolverTest {
         val a = ctx.mkRegisterReading(0, addressSort)
         val b1 = ctx.mkRegisterReading(1, addressSort)
         val b2 = ctx.mkRegisterReading(2, addressSort)
-
         val c = ctx.mkRegisterReading(3, addressSort)
+
         pc += mkHeapRefEq(a, nullRef).not() and
             mkHeapRefEq(b1, nullRef).not() and
             mkHeapRefEq(b2, nullRef).not() and
@@ -226,6 +226,39 @@ class TypeSolverTest {
         }
     }
 
+    @Test
+    fun `Test symbolic ref -- expressions to assert correctness about null`(): Unit = with(ctx) {
+        val a = ctx.mkRegisterReading(0, addressSort)
+        val b = ctx.mkRegisterReading(1, addressSort)
+        val c = ctx.mkRegisterReading(2, addressSort)
+
+        pc += mkIsExpr(a, interfaceAB)
+        pc += mkIsExpr(b, interfaceBC1)
+        pc += mkIsExpr(c, interfaceAC)
+
+        // it's overcomplicated a == c && b == c
+        pc += (mkHeapRefEq(a, c) or mkHeapRefEq(b, c)) and (!mkHeapRefEq(a, c) or !mkHeapRefEq(b, c)).not()
+
+        val resultBeforeNotNullConstraints = solver.check(pc, useSoftConstraints = false)
+        val model = assertIs<USatResult<UModelBase<Field, TestType>>>(resultBeforeNotNullConstraints).model
+
+        assertIs<USatResult<UModelBase<Field, TestType>>>(resultBeforeNotNullConstraints)
+
+        val concreteA = assertIs<UConcreteHeapRef>(model.eval(a)).address
+        val concreteB = assertIs<UConcreteHeapRef>(model.eval(b)).address
+        val concreteC = assertIs<UConcreteHeapRef>(model.eval(c)).address
+
+        val someIsNull = concreteA == 0 || concreteB == 0 || concreteC == 0
+        val aEqualsCOrBEqualsC = concreteA == concreteC || concreteB == concreteC
+        assertTrue(someIsNull && aEqualsCOrBEqualsC)
+
+        pc += mkOrNoSimplify(mkHeapRefEq(a, nullRef).not(), falseExpr)
+        pc += mkOrNoSimplify(mkHeapRefEq(b, nullRef).not(), falseExpr)
+
+        val resultWithNotNullConstraints = solver.check(pc, useSoftConstraints = false)
+        assertIs<UUnsatResult<UModelBase<Field, TestType>>>(resultWithNotNullConstraints)
+    }
+
     @Test
     @Disabled("Support propositional type variables")
     fun `Test symbolic ref -- not instance of constraint`(): Unit = with(ctx) {