From 38166ae13a04504295f77701c69b675cfc2ca02b Mon Sep 17 00:00:00 2001
From: Nicolas Setton <setton@adacore.com>
Date: Mon, 18 Jun 2018 14:01:25 -0400
Subject: [PATCH] Run SPARK with --level=0 --no-axiom-guard

---
 compile_server/app/checker.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/compile_server/app/checker.py b/compile_server/app/checker.py
index 818e9ed..024c746 100644
--- a/compile_server/app/checker.py
+++ b/compile_server/app/checker.py
@@ -146,7 +146,8 @@ def check_program(request):
         doctor_main_gpr(tempd, main)
 
     # Run the command(s) to check the program
-    command = ["gnatprove", "-P", "main", "--checks-as-errors", "--level=2"]
+    command = ["gnatprove", "-P", "main", "--checks-as-errors",
+               "--level=0", "--no-axiom-guard"]
 
     # Process extra_args
     if 'extra_args' in received_json: