From 21933f899a478e73b18350132bdb952eb3c22998 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Mon, 30 Mar 2020 11:44:40 +0800
Subject: [PATCH] simplexport: build SimplExportAndRefine on CSpec

It looks like generated files are missing if built on SimplExport direclty.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
---
 proof/ROOT | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/proof/ROOT b/proof/ROOT
index 1dd515fc2..5b2cbd520 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -199,7 +199,9 @@ session Bisim in bisim = AInvs +
 (*
  * Binary Verification Input Step
 *)
-session SimplExportAndRefine in "asmrefine" = SimplExport +
+session SimplExportAndRefine in "asmrefine" = CSpec +
+  sessions
+    SimplExport
   theories
     "SEL4GraphRefine"