]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Fix: missing check to avoid stepping on vars of non positive arity
authoracondolu <andrea.condoluci@unibo.it>
Thu, 13 Jul 2017 17:05:39 +0000 (19:05 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 09:08:51 +0000 (11:08 +0200)
(cherry picked from commit 58f1518398346a81ccd8d0b14a14565b8bff5276)

ocaml/lambda4.ml

index 62837b2fd9842ce177e507737d3b8ffd89a6ea4c..83f1c427cc56164cb31ffc117dd1bbc9ea656f39 100644 (file)
@@ -526,7 +526,10 @@ let auto_instantiate (n,p) =
        prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
        x
   with
-   Not_found -> x in
+   Not_found ->
+    let arity_of_x = max_arity_tms x (all_terms p) in
+    assert (Util.option_get arity_of_x > 0); 
+    x in
 (* Instantiate in decreasing order of compute_special_k
 1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s
 let x =