aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-25 14:31:15 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:42:01 +0200
commit87910d7be9bd50de4db80f70c6e287c7c7994460 (patch)
treeff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /plugins/omega
parent5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff)
Fix 4.04 warnings
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/omega.ml10
1 files changed, 6 insertions, 4 deletions
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index bd991a955..334b03de1 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -330,11 +330,13 @@ let omega_mod a b = a - b * floor_div (two * a + b) (two * b)
let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 =
let e = original.body in
let sigma = new_var_id () in
+ if e == [] then begin
+ display_system print_var [original] ; failwith "TL"
+ end;
let smallest,var =
- try
- List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p))
- (abs (List.hd e).c, (List.hd e).v) (List.tl e)
- with Failure "tl" -> display_system print_var [original] ; failwith "TL" in
+ List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p))
+ (abs (List.hd e).c, (List.hd e).v) (List.tl e)
+ in
let m = smallest + one in
let new_eq =
{ constant = omega_mod original.constant m;