* Report error when a theorem is false

6402581d · Jerome Hugues · 30fa0438 · 6402581d
Commit 6402581d authored Apr 19, 2016 by Jerome Hugues
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

src/backends/ocarina-backends-real.adb src/backends/ocarina-backends-real.adb +4 -0

No files found.
--- a/src/backends/ocarina-backends-real.adb
+++ b/src/backends/ocarina-backends-real.adb
@@ -366,6 +366,10 @@ package body Ocarina.Backends.REAL is
         Success := False;
      end if;

+      if not Success then
+         N_Errors := N_Errors + 1;
+      end if;
+
      Write_Line
        ("theorem " &
         Get_Name_String (Name (Identifier (R))) &