diff --git a/protocols/misc/tls/tls-paulson-avispa.spdl b/protocols/misc/tls/tls-paulson-avispa.spdl
index 5fc352d..19c11cc 100644
--- a/protocols/misc/tls/tls-paulson-avispa.spdl
+++ b/protocols/misc/tls/tls-paulson-avispa.spdl
@@ -15,7 +15,9 @@ secret unkeygen: Function;
 inversekeys(keygen, unkeygen);
 
 const pa,pb: Params;
+const Alice,Bob: Agent;
 const Terence: Agent;
+const Sally: Agent;
 const false,true: Bool;
 
 
diff --git a/src/compiler.c b/src/compiler.c
index 5fbeed2..676ef4c 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -2213,8 +2213,10 @@ preprocess (const System sys)
   /*
    * Check well-formedness
    */
+  /* TODO Temporarily disabled wellformedness check (well-formedness) after Simon bug reporting.
   if (sys->knowledgedefined)
     {
       checkWellFormed (sys);
     }
+  */
 }
diff --git a/src/intruderknowledge.c b/src/intruderknowledge.c
index 035d1c9..f298cfb 100644
--- a/src/intruderknowledge.c
+++ b/src/intruderknowledge.c
@@ -115,6 +115,13 @@ anySubTerm (Term t, Termlist sublist)
 void
 initialIntruderKnowledge (const System sys)
 {
+  /*
+  TODO this is buggy and leads to a segfault with Simon's example (bug report for wellformedness check)
+  Disabled for now.
+  ./scyther-linux simple-challenge-SEGFAULT.spdl
+  */
+  return;
+
   /*
    * display initial role knowledge
    */