#define NULL (void*)0

__attribute__ ((noinline)) int nondet() { return 0; }

#ifdef CONFIG_SMP
int smp_found_config; /* found an SMP configuration at boot time ? */
#endif

void enable_IR_x2apic(void)
{
  static char c;
  static char *ptr = &c;

  *ptr = 'a';
  if (ptr)
    ptr = NULL;
}

int APIC_init_uniprocessor(void)
{
  enable_IR_x2apic(); // (6) ERROR: enable_IR_x2apic() is not idempotent
}

#ifdef CONFIG_SMP
int smp_sanity_check()
{
  if (!smp_found_config)
    APIC_init_uniprocessor(); // (5)
  return 0;
}

void native_smp_prepare_cpus()
{
  enable_IR_x2apic(); // (3) first call
  smp_sanity_check(); // (4)
}
#endif

int main(void)
{
#ifdef CONFIG_SMP
  smp_found_config = nondet(); // (1)
  native_smp_prepare_cpus(); // (2)
#endif
  return 0;
}

diff --git a/simple/472a474.c b/simple/472a474.c
--- a/simple/472a474.c
+++ b/simple/472a474.c
@@ -19,7 +19,9 @@
 
 int APIC_init_uniprocessor(void)
 {
+#ifndef CONFIG_SMP
   enable_IR_x2apic(); // (6) ERROR: enable_IR_x2apic() is not idempotent
+#endif
 }
 
 #ifdef CONFIG_SMP

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

int main(int argc, char** argv)
{
#ifdef CONFIG_SMP
  int smp_found_config;
  smp_found_config = false;
//  native_smp_prepare_cpus();
  static int called = 0;

  called++;
  if (called > 1) 
    do { fprintf(stderr, "panic!\n"); exit(1); } while(0);
  
  if (!smp_found_config) {
      called = 0;

      called++;
      if (called > 1) 
        do { fprintf(stderr, "panic!\n"); exit(1); } while(0);
  }
#endif
  return 0;
}

. call arch/x86/kernel/smpboot.c:1071:native_smp_prepare_cpus()
. 1095: enable_IR_x2apic();
. 1098: if (smp_sanity_check(max_cpus) < 0)
.. call arch/x86/kernel/smpboot.c:954:smp_sanity_check()
.. 997: if (!smp_found_config && !acpi_lapic) {
// do not find SMP configuration, i.e. non-SMP CPU
.. 1001: if (APIC_init_uniprocessor())
... call arch/x86/kernel/apic/apic.c:1616:APIC_init_uniprocessor()
... ERROR 1643: enable_IR_x2apic();