rt crefine: switch on quick_and_dirty for RISCV64 CRefine

Allow sorries during development. Signed-off-by: Michael McInerney <[email protected]>
seL4 · Oct 19, 2023 · 3d978d7 · 3d978d7
1 parent c84781c
commit 3d978d7
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/proof/Makefile b/proof/Makefile
@@ -15,6 +15,11 @@ ifeq "$(L4V_ARCH)" "AARCH64"
   export REFINE_QUICK_AND_DIRTY=1
 endif
 
+# Allow sorry command in RISCV64 CRefine during development:
+ifeq "$(L4V_ARCH)" "RISCV64"
+  export CREFINE_QUICK_AND_DIRTY=1
+endif
+
 #
 # Setup heaps.
 #