llvm: Fix validity predicate for memory reads with symbolic block num…

…bers

Previously, this case returned the concretely-true predicate. This is
incorrect, as `isAllocatedGeneric` takes an argument `inAlloc`, which is
supposed to be applied to the `AllocInfo` of the allocation with the
matching block number, as it is in the other branch.

Mea culpa, looks like I introduced this bug long ago.

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs

@@ -252,12 +252,7 @@ isAllocatedGeneric sym inAlloc blk = go (pure (falsePred sym)) (pure (truePred s
                        Just True ->
                          -- This is where where this block was allocated, and it
                          -- couldn't have been freed before it was allocated.
-                         --
-                         -- NOTE(lb): It's not clear to me that this branch is
-                         -- reachable: If the equality test can succeed
-                         -- concretely, wouldn't asNat have returned a Just
-                         -- above? In either case, this answer should be sound.
-                         return (truePred sym, truePred sym)
+                         (, truePred sym) <$> inAlloc ba
                        Just False -> k
                        Nothing ->
                          do (fallback', fallbackFreed') <- k