/* This tries to havoc to a null pointer.
 * It will have a null pointer dereference violation.
 */
#include<civlc.cvh>
#include<stdio.h>

int main(){
  int x;
  int* p=NULL;

  $havoc(p);//p couldn't be a null pointer
}