First pass on ecCircuits error handling

EasyCrypt · Nov 22, 2024 · fa56c97 · fa56c97
1 parent 1d04ab9
commit fa56c97
Show file tree

Hide file tree

Showing 2 changed files with 306 additions and 219 deletions.
diff --git a/libs/lospecs/hlaig.ml b/libs/lospecs/hlaig.ml
@@ -59,7 +59,9 @@ end
 (* Assumes circuit inputs have already been appropriately renamed *)
 module MakeSMTInterface(SMT: SMTInstance) : SMTInterface = struct
   let circ_equiv (r1 : Aig.reg) (r2 : Aig.reg) (pcond : Aig.node) (inps: (int * int) list) : bool =
-    assert ((List.compare_length_with r1 0 > 0) && (List.compare_length_with r2 0 > 0));
+    if not ((List.compare_length_with r1 0 > 0) && (List.compare_length_with r2 0 > 0)) then
+      (Format.eprintf "Sizes differ in circ_equiv"; false)
+    else
     let bvvars : SMT.bvterm Map.String.t ref = ref Map.String.empty in
 
     let rec bvterm_of_node : Aig.node -> SMT.bvterm =