diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
index 12354709d68f84e247c7b3678b41dfcb4e2a1bab..4a7ce472c475d484b5deb98e5b5654d5b4338b43 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/DisproverReasoner.java
@@ -107,9 +107,18 @@ public class DisproverReasoner implements IReasoner {
 
 		// find the IEventBProject belonging to the sequent
 		IPOSequent origin = (IPOSequent) sequent.getOrigin();
-		IRodinProject project = origin.getRodinProject();
-		IEventBProject evbProject = (IEventBProject) project
-				.getAdapter(IEventBProject.class);
+		
+		IEventBProject evbProject;
+		
+		if (origin==null) { // no origin available; seems to happen in Rodin 3.5RC upon startup
+		   System.out.println("No origin available for sequent")
+		   // throw new InterruptedException(); // Should we do this instead of trying to work with null project?
+		   evbProject = null;
+		} else {
+			IRodinProject project = origin.getRodinProject();
+			evbProject = (IEventBProject) project
+					.getAdapter(IEventBProject.class);
+		}
 		ICounterExample counterExample = DisproverCommand.disprove(
 				Animator.getAuxAnimator(), evbProject, allHypotheses,
 				selectedHypotheses, goal, timeoutFactor, context, pm);
diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/command/DisproverLoadCommand.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/command/DisproverLoadCommand.java
index faf38c749654af9f32dd1961db863cc42c023748..d4d437ffeda8f969b9510f1e2a9aad43961e3fb6 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/command/DisproverLoadCommand.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/command/DisproverLoadCommand.java
@@ -73,6 +73,7 @@ public final class DisproverLoadCommand implements IComposableCommand {
 	private boolean theoriesUsed() throws TranslationFailedException {
 		try {
 			final IRodinElement[] elements;
+			if (project==null) { return false;}
 			elements = project.getRodinProject().getChildren();
 			for (IRodinElement element : elements) {
 				if (element instanceof IRodinFile) {