#include <assert.h>

// To avoid constant propagation
__attribute__ ((noinline)) int nondet() { return 42; }

#ifdef CONFIG_VLAN_8021Q
_Bool vlan_hwaccel_do_receive()
{
  // do something
  return 1;
}
#else
_Bool vlan_hwaccel_do_receive()
{
  assert(0); // (4) ERROR
  return 0;
}
#endif

int __netif_receive_skb()
{
  if (nondet())
	{
	  vlan_hwaccel_do_receive(); // (3)
	}
  return 0;
}

int netif_receive_skb()
{
#ifdef CONFIG_RPS
  return __netif_receive_skb(); // (2)
#else
  return __netif_receive_skb(); // (2)
#endif
}

int main(void)
{
  netif_receive_skb(); // (1)
  return 0;
}

diff --git a/simple/0988c4c.c b/simple/0988c4c.c
--- a/simple/0988c4c.c
+++ b/simple/0988c4c.c
@@ -13,7 +13,6 @@
 #else
 _Bool vlan_hwaccel_do_receive()
 {
-  assert(0); // (4) ERROR
   return 0;
 }
 #endif

#include <assert.h>
#include <stdbool.h>
#include <stdlib.h>

int main(int argc, char** argv)
{
//  netif_receive_skb();
  if (rand() % 2) {
    #ifdef CONFIG_VLAN_8021Q
    // do something
    return true;
    #else
    assert(false); // ERROR
    return false;
    #endif
  }
  return 0;
}

. call net/core/dev.c:2602:netif_rx()
// reads a packet from a device driver and queues it to be processed by upper layers
// at some point netif_receive_skb() will be invoked ...
. call net/core/dev.c:3039:netif_receive_skb()
. 3067: return __netif_receive_skb(skb);
.. call net/core/dev.c:2887:__netif_receive_skb()
.. 2972: if (vlan_tx_tag_present(skb)) {
.. 2977: if (vlan_hwaccel_do_receive(&skb)) {
... [!VLAN_8021Q] call include/linux/if_vlan.h:169:vlan_hwaccel_do_receive()
... ERROR [!VLAN_8021Q] BUG();