diff --git a/domains/Affines.ml b/domains/Affines.ml index 33547050..29f1dd8a 100644 --- a/domains/Affines.ml +++ b/domains/Affines.ml @@ -7,6 +7,8 @@ open Partition open Functions open Numerical +module VarMap = Mapext.Make(Var) + module Affine (B : PARTITION) : FUNCTION = struct module B = B @@ -160,6 +162,54 @@ module Affine (B : PARTITION) : FUNCTION = struct | Bot, _ | _, Top -> true | _ -> false + let getCompressed cs c nc f01 f02 : f option = + let fvars1, fvars2 = f01.vars, f02.vars in + match f01.ranking, f02.ranking with + | Fun f1, Fun f2 -> begin + let vars1 = ref VarMap.empty in + let vars2 = ref VarMap.empty in + Linexpr1.iter + (fun c v -> + if not (Coeff.is_zero c) && List.exists (fun v1 -> String.compare (Var.to_string v) v1.varId = 0) fvars1 then + vars1 := VarMap.add v c !vars1) + f1 ; + Linexpr1.iter + (fun c v -> + if not (Coeff.is_zero c) && List.exists (fun v2 -> String.compare (Var.to_string v) v2.varId = 0) fvars2 then + vars2 := VarMap.add v c !vars2) + f2 ; + let le1 = Linexpr1.make f01.env in + let le2 = Linexpr1.make f02.env in + let ler = Linexpr1.make f1.env in + let arr1 = Lincons1.array_make f01.env (List.length cs + 1) in + let arr2 = Lincons1.array_make f01.env (List.length cs + 1) in + Lincons1.array_set arr1 0 c; + Lincons1.array_set arr2 0 nc; + List.iteri (fun i c -> Lincons1.array_set arr1 (i + 1) c; Lincons1.array_set arr2 (i + 1) c) cs; + let cs1 = Abstract1.of_lincons_array manager f01.env arr1 in + let cs2 = Abstract1.of_lincons_array manager f02.env arr2 in + VarMap.iter2o + (fun v1 c1 -> Linexpr1.set_coeff le1 v1 c1) + (fun v2 c2 -> Linexpr1.set_coeff le2 v2 c2) + (fun v c1 c2 -> + if Coeff.equal c1 c2 then Linexpr1.set_coeff ler v c1 + else (Linexpr1.set_coeff le1 v c1; Linexpr1.set_coeff le2 v c2)) + !vars1 !vars2; + Linexpr1.set_cst le1 (Linexpr1.get_cst f1); + Linexpr1.set_cst le2 (Linexpr1.get_cst f2); + let i1 = Abstract1.bound_linexpr manager cs1 le1 in + let i2 = Abstract1.bound_linexpr manager cs2 le2 in + if Scalar.is_infty i1.sup = 0 && Scalar.is_infty i2.sup = 0 + then if Scalar.cmp i1.sup i2.sup > 0 then begin + Linexpr1.set_cst ler (Coeff.Scalar i1.sup); + Some { f01 with ranking = Fun ler } + end else begin + Linexpr1.set_cst ler (Coeff.Scalar i2.sup); + Some { f02 with ranking = Fun ler } + end else None + end + | _ -> None + (**) let join_ranking k b f1 f2 = diff --git a/domains/DecisionTree.ml b/domains/DecisionTree.ml index 4e18e5e2..96b7c561 100644 --- a/domains/DecisionTree.ml +++ b/domains/DecisionTree.ml @@ -28,6 +28,8 @@ let evolvethr = ref 0 let tracebwd = ref false let retrybwd = ref 5 +let tracewiden = false + (** The ranking functions abstract domain is an abstract domain functor T. It is parameterized by an auxiliary abstract domain for linear constraints C, and an auxiliary abstract domains for functions F, both parameterized by @@ -68,6 +70,8 @@ struct upper bounds on the number of program execution steps to termination. *) type tree = Bot | Leaf of F.f | Node of L.t * tree * tree + exception GetOut of tree*tree + (** An element of the ranking functions abstract domain. *) type t = { domain : B.t option; (* current reachable program states *) @@ -84,11 +88,11 @@ struct let print_tree vars fmt t = let rec aux ind fmt t = match t with - | Bot -> Format.fprintf fmt "\n%sNIL" ind - | Leaf f -> Format.fprintf fmt "\n%sLEAF %a" ind F.print f - | Node ((c,_),l,r) -> Format.fprintf fmt "\n%sNODE %a%a%a" ind - (C.print vars) c (aux (ind ^ " ")) l (aux (ind ^ " ")) r - in aux "" fmt t + | Bot -> Format.fprintf fmt "NIL" + | Leaf f -> Format.fprintf fmt "LEAF %a" F.print f + | Node ((c,_),l,r) -> Format.fprintf fmt "NODE %a\n%s+ %a\n%s` %a" + (C.print vars) c ind (aux (ind ^ "| ")) l ind (aux (ind ^ " ")) r + in Format.fprintf fmt "\n%a" (aux "") t (** Prints a tree in graphviz 'dot' format for visualization. @@ -521,8 +525,7 @@ struct else true else false | COMPUTATIONAL -> - F.isLeq k b f1 f2 (* forall x: f1(x) <= f2(x) *) - | _ -> raise (Invalid_argument ("Learning order not defined for tree")) ) + F.isLeq k b f1 f2 (* forall x: f1(x) <= f2(x) *) ) | Node ((c1,nc1),l1,r1), Node((c2,nc2),l2,r2) when (C.isEq c1 c2) -> (aux (l1,l2) (c1::cs)) && (aux (r1,r2) (nc1::cs)) @@ -623,7 +626,6 @@ struct let fBotLeftRight = match k with | APPROXIMATION -> fun _ _ -> Bot (* use NIL if at least one leaf is NIL *) | COMPUTATIONAL -> fun _ _ -> botLeaf (* use bottom leaf if at least one leaf is nil*) - | _ -> raise (Invalid_argument "Should not call Learning meet on decision trees") in let fLeaf cs f1 f2 = let b = match domain with @@ -857,14 +859,12 @@ struct let domain = t1.domain in let env = t1.env in let vars = t1.vars in + let inner_b cs = match domain with None -> B.inner env vars cs | Some domain -> B.meet (B.inner env vars cs) domain in let t1 = t1.tree and t2 = t2.tree in let rec widen_right (t1,t2) cs = match t1,t2 with | Leaf f1,Leaf f2 -> - let b = match domain with - | None -> B.inner env vars cs - | Some domain -> B.meet (B.inner env vars cs) domain in - + let b = inner_b cs in if F.isLeq COMPUTATIONAL b f1 f2 then t2 else Leaf (F.top env vars) | Node((c1,nc1),l1,r1),Node((c2,nc2),l2,r2) when (C.isEq c1 c2) (* c1 = c2 *) -> @@ -872,12 +872,12 @@ struct let r = widen_right (r1,r2) (nc1::cs) in Node((c2,nc2),l,r) | Node((c1,nc1),l1,r1),Node((c2,_),_,_) when (C.isLeq c1 c2) (* c1 < c2 *) -> - let bcs = B.inner env vars cs in - let bc1 = B.inner env vars [c1] in + let bcs = inner_b cs in + let bc1 = inner_b [c1] in if (B.isLeq bcs bc1) then (* c1 is redundant *) widen_right (l1,t2) cs else (* c1 is not redundant *) - let bnc1 = B.inner env vars [nc1] in + let bnc1 = inner_b [nc1] in if (B.isLeq bcs bnc1) then (* nc1 is redundant *) widen_right (r1,t2) cs else (* nc1 is not redundant *) let l = widen_right (l1, t2) (c1 :: cs) in @@ -889,12 +889,12 @@ struct Node((c2,nc2),l,r) | Node ((c1,nc1),l1,r1),_ -> - let bcs = B.inner env vars cs in - let bc1 = B.inner env vars [c1] in + let bcs = inner_b cs in + let bc1 = inner_b [c1] in if (B.isLeq bcs bc1) then (* c1 is redundant *) widen_right (l1,t2) cs else (* c1 is not redundant *) - let bnc1 = B.inner env vars [nc1] in + let bnc1 = inner_b [nc1] in if (B.isLeq bcs bnc1) then (* nc1 is redundant *) widen_right (r1,t2) cs else (* nc1 is not redundant *) let l = widen_right (l1, t2) (c1 :: cs) in @@ -910,30 +910,30 @@ struct match t1,t2 with | Bot,Bot -> Bot | Leaf f1,Leaf f2 -> - let b = match domain with | None -> B.inner env vars cs | Some domain -> B.meet (B.inner env vars cs) domain in + let b = inner_b cs in Leaf (F.widen ~jokers:(if !retrybwd > 0 then (jokers + !retrybwd - 1) / !retrybwd else 0) b f1 f2) | Node ((c1,nc1),l1,r1),Node((c2,nc2),l2,r2) when (C.isEq c1 c2) (* c1 = c2 *) -> Node ((c1,nc1),widen_up (l1,l2) (c1::cs),widen_up (r1,r2) (nc1::cs)) | Node ((c1,nc1),l1,r1),Node((c2,_),_,_) when (C.isLeq c1 c2) (* c1 < c2 *) -> - let bcs = B.inner env vars cs in - let bc1 = B.inner env vars [c1] in + let bcs = inner_b cs in + let bc1 = inner_b [c1] in if (B.isLeq bcs bc1) then (* c1 is redundant *) widen_up (l1,t2) cs else (* c1 is not redundant *) - let bnc1 = B.inner env vars [nc1] in + let bnc1 = inner_b [nc1] in if (B.isLeq bcs bnc1) then (* nc1 is redundant *) widen_up (r1,t2) cs else (* nc1 is not redundant *) Node ((c1, nc1), widen_up (l1, t2) (c1 :: cs), widen_up (r1, t2) (nc1 :: cs)) | Node ((c1,_),_,_),Node((c2,nc2),l2,r2) when (C.isLeq c2 c1) (* c1 > c2 *) -> Node((c2,nc2),widen_up (t1,l2) (c2::cs),widen_up (t1,r2) (nc2::cs)) | Node ((c1,nc1),l1,r1),_ -> - let bcs = B.inner env vars cs in - let bc1 = B.inner env vars [c1] in + let bcs = inner_b cs in + let bc1 = inner_b [c1] in if (B.isLeq bcs bc1) then (* c1 is redundant *) widen_up (l1,t2) cs else (* c1 is not redundant *) - let bnc1 = B.inner env vars [nc1] in + let bnc1 = inner_b [nc1] in if (B.isLeq bcs bnc1) then (* nc1 is redundant *) widen_up (r1,t2) cs else (* nc1 is not redundant *) Node ((c1, nc1), widen_up (l1, t2) (c1 :: cs), widen_up (r1, t2) (nc1 :: cs)) | _,Node((c2,nc2),l2,r2) -> Node((c2,nc2),widen_up (t1,l2) (c2::cs),widen_up (t1,r2) (nc2::cs)) @@ -942,103 +942,165 @@ struct let widen (t1,t2) = let prev = t1 in let lbl = LSet.elements (tree_labels t2) in - let rec leaves p t ls cs = - match t,ls with - | Bot,_ -> [] - | Leaf f,[] -> - let b = match domain with | None -> B.inner env vars cs | Some domain -> B.meet (B.inner env vars cs) domain in - if (F.defined f) && not (B.isBot b) && not (F.isEq b f (F.reset f)) then [b,f] else [] - | Leaf _,(c,nc)::ls -> - let h = List.hd p in - if (h = 1) then leaves (List.tl p) t ls (c::cs) - else if (h = 2) then leaves (List.tl p) t ls (nc::cs) - else leaves (List.tl p) t ls cs - | Node ((c1,nc1),l1,r1),(c,_)::ls when (C.isEq c1 c) -> - let h = List.hd p in - if (h = 2) then leaves (List.tl p) r1 ls (nc1::cs) - else leaves (List.tl p) l1 ls (c1::cs) - | Node ((c1,_),_,_),(c,nc)::ls when (C.isLeq c c1) -> - let h = List.hd p in - if (h = 1) then leaves (List.tl p) t ls (c::cs) - else if (h = 2) then leaves (List.tl p) t ls (nc::cs) - else leaves (List.tl p) t ls cs - | _ -> raise (Invalid_argument "widen:leaves:") + let () = + if tracewiden && !tracebwd then begin + List.iter (fun (c,_nc) -> Format.printf "%a " Lincons1.print c) lbl; + match domain with + | None -> () + | Some domain -> Format.printf "\nDomain: %a@." B.print domain + end in + let extend1 b2 f20 f2 (b1,f1) = + if !tracebwd then + begin + Format.fprintf Format.std_formatter "EXTEND\n"; + Format.fprintf Format.std_formatter "%a? %a\n" B.print b1 F.print f1; + Format.fprintf Format.std_formatter "%a? %a\n" B.print b2 F.print f20; + Format.fprintf Format.std_formatter "%a? %a\n\n" B.print b2 F.print (F.extend b1 b2 f1 f20) + end; + F.join COMPUTATIONAL b2 (F.extend b1 b2 f1 f20) f2 in - let rec adjacent p1 p2 = - match p2 with - | [] -> leaves p1 prev lbl [] - (* List.iter (fun p -> Format.fprintf Format.std_formatter "%s " (string_of_int p)) p1; - Format.fprintf Format.std_formatter "\n"; - leaves p1 prev lbl [] *) - | h::ps -> - (match h with - | 1 -> (leaves (p1@[2]@ps) prev lbl []) @ (adjacent (p1@[1]) ps) - (* List.iter (fun p -> Format.fprintf Format.std_formatter "%s " (string_of_int p)) (p1@[2]@ps); - Format.fprintf Format.std_formatter "\n"; - (leaves (p1@[2]@ps) prev lbl []) @ (adjacent (p1@[1]) ps) *) - | 2 -> (leaves (p1@[1]@ps) prev lbl []) @ (adjacent (p1@[2]) ps) - (* List.iter (fun p -> Format.fprintf Format.std_formatter "%s " (string_of_int p)) (p1@[1]@ps); - Format.fprintf Format.std_formatter "\n"; - (leaves (p1@[1]@ps) prev lbl []) @ (adjacent (p1@[2]) ps) *) - | _ -> adjacent (p1@[0]) ps) + let rec leaf p (* labels + path *) t leafcs cs = + let select ((c,nc),(h,_)) cs = + if h then c::cs + else nc::cs in + let () = + if tracewiden && cs = [] && !tracebwd then begin + Format.printf "leaf"; + List.iter (fun (_,h) -> Format.printf " %b(%b)" (fst h) (snd h)) p; + Format.printf "%a@." (print_tree vars) t + end in + match t with + | Bot -> None + | Leaf f -> + let cs = + let rec inner p cs = match p with + | [] -> cs + | h::p -> inner p (select h cs) + in inner p cs in + let leafb = inner_b leafcs in + let b = inner_b cs in + let () = + if tracewiden && !tracebwd then begin + Format.printf "%a [%b] // %a [%b] // %b => %a@." + F.print f (F.defined f) + B.print b (not (B.isBot b)) + (not (F.isEq b f (F.reset f))) + B.print leafb + end in + if (F.defined f) && not (B.isBot b) && not (F.isEq b f (F.reset f)) then Some (leafb, f) else None + | Node ((c1,_),l1,r1) -> begin match p with + | [] -> raise (Invalid_argument "widen:leaf:") + | ((c,_),(s,_) as h)::p -> + if C.isEq c1 c + then leaf p (if s then l1 else r1) (select h leafcs) (select h cs) + else leaf p t leafcs (select h cs) + end in - let rec extend (b2,f2) bfs = - match bfs with - | [] -> f2 - | (b1,f1)::bfs -> - if !tracebwd then - begin - Format.fprintf Format.std_formatter "EXTEND\n"; - Format.fprintf Format.std_formatter "%a? %a\n" B.print b1 F.print f1; - Format.fprintf Format.std_formatter "%a? %a\n" B.print b2 F.print f2; - Format.fprintf Format.std_formatter "%a? %a\n\n" B.print b2 F.print (F.extend b1 b2 f1 f2) - end; - F.join COMPUTATIONAL b2 (F.extend b1 b2 f1 f2) (extend (b2,f2) bfs) + let rec adjacent leafb f2 p1 p2 acc = + let () = + if tracewiden && !tracebwd && p1 = [] then begin + Format.printf "adjacent"; + List.iter (fun (_, (h, r)) -> Format.printf " %b(%b)" h r) p2; + Format.printf "@." + end in + match p2 with + | [] -> acc + | (p, (b, true)) :: ps -> adjacent leafb f2 ((p, (b, true)) :: p1) ps acc + | (p, (b, false)) :: ps -> begin + let acc = match leaf (List.rev_append p1 ((p, (not b, false)) :: ps)) prev [] [] with + | None -> acc + | Some (b, l) -> extend1 leafb f2 acc (b, l) + in adjacent leafb f2 ((p, (b, false)) :: p1) ps acc + end in let rec merge (t1,t2) cs = match t1,t2 with | _,Bot -> t1 | Bot,_ -> t2 - | Leaf f1,Leaf f2 -> Leaf (F.join COMPUTATIONAL (B.inner env vars cs) f1 f2) + | Leaf f1,Leaf f2 -> Leaf (F.join COMPUTATIONAL (inner_b cs) f1 f2) | Node ((c1,nc1),l1,r1),Node((c2,nc2),l2,r2) when (C.isEq c1 c2) (* c1 = c2 *) -> let l = merge (l1,l2) (c1::cs) in let r = merge (r1,r2) (nc1::cs) in Node ((c1,nc1),l,r) | _ -> raise (Invalid_argument "widen:merge:") in - let rec aux p (* path *) ls (* labels *) (t1,t2) cs = - match t1, t2, ls with - | Bot, Bot, _ -> Bot - | Leaf f1, Leaf f2, _ -> - let b = match domain with | None -> B.inner env vars cs | Some domain -> B.meet (B.inner env vars cs) domain in - if (B.isBot b) then Bot - else if (F.isEq b f1 f2) then t2 - else - let p = List.rev p @ List.map (fun _ -> 0) ls in - let bfs = adjacent [] p in - Leaf (extend (b, f2) bfs) - | Node ((c1, nc1), l1, r1), - Node ((c2, nc2), l2, r2), - (c, _) :: ls - when C.isEq c1 c2 && C.isEq c1 c -> - let l = aux (1::p) ls (l1, l2) (c1 :: cs) in - let r = aux (2::p) ls (r1, r2) (nc1 :: cs) in - Node ((c1,nc1),l,r) - | Node ((c1, _), _, _), - Node ((c2, _), _, _), - (c, nc) :: ls - when C.isEq c1 c2 && C.isLeq c c1 -> - let bcs = B.inner env vars cs in - let bc = B.inner env vars [c] in - if (B.isLeq bcs bc) - then (* c is redundant *) - aux (0 :: p) ls (t1, t2) cs - else (* c is not redundant *) - merge (aux (1 :: p) ls (t1, t2) (c :: cs), - aux (2 :: p) ls (t1, t2) (nc :: cs)) cs - | Bot, _, _ | _, Bot, _ | _, _, _ -> Bot + let rec aux p (* path *) ls (* labels *) (t1,t2) leafcs cs = + (* The path also contains the associated label *) + let () = + if tracewiden && !tracebwd then begin + List.iter (fun (_, (h, r)) -> Format.printf "%b(%b) " h r) p; + Format.printf "%a%a@.cs = [" (print_tree vars) t1 (print_tree vars) t2; + List.iter (fun c -> Format.printf "%a " Lincons1.print c) cs; + Format.printf "]@." + end in + match t1, t2 with + | Bot, _ | _, Bot -> Bot + | Leaf _, Node _ + | Node _, Leaf _ -> raise (Invalid_argument "widen:aux:") + | Leaf f1, Leaf f2 -> + let leafb = inner_b leafcs in + let b = inner_b cs in + let () = + if tracewiden && !tracebwd then begin + Format.printf "Leaf + Leaf with b = %a {%a} [%b]@." B.print b B.print leafb (F.isEq b f1 f2) + end in + if (B.isBot b) then Bot + else if (F.isEq b f1 f2) then t2 + else + let rec aux2 p ls cs acc = match ls with (* finish the path, then extend *) + | [] -> adjacent leafb f2 [] (List.rev p) acc (* path finished *) + | (c, nc) :: ls -> (* extend the path *) + let bcs = B.inner env vars cs in + let bc = B.inner env vars [c] in + let bnc = B.inner env vars [nc] in + let leqc = B.isLeq bcs bc in + let leqnc = B.isLeq bcs bnc in + let () = + if tracewiden && !tracebwd then begin + Format.printf "Path extension with bcs = %a // bc = %a // bnc = %a [%b/%b]@." B.print bcs B.print bc B.print bnc leqc leqnc + end in + if leqc + then (* c is redundant *) + aux2 (((c, nc), (true, true)) :: p) ls cs acc + else if leqnc + then (* nc is redundant *) + aux2 (((c, nc), (false, true)) :: p) ls cs acc + else (* c and nc are not redundant; mark them as such anyway to avoid taking the current leaf *) + aux2 (((c, nc), (false, true)) :: p) ls (nc :: cs) (aux2 (((c, nc), (true, true)) :: p) ls (c :: cs) acc) + in + Leaf (aux2 p ls cs f2) + | Node ((c1, _), l1, r1), Node ((c2, _), l2, r2) -> + if not (C.isEq c1 c2) then raise (Invalid_argument "widen:aux:") + else begin match ls with + | [] -> raise (Invalid_argument "widen:aux:") + | (c, nc) :: ls -> + if C.isEq c1 c then begin + let l = aux (((c, nc), (true, false))::p) ls (l1, l2) (c :: leafcs) (c :: cs) in + let r = aux (((c, nc), (false, false))::p) ls (r1, r2) (nc :: leafcs) (nc :: cs) in + Node ((c,nc),l,r) + end else if C.isLeq c c1 then begin + let bcs = B.inner env vars cs in + let bc = B.inner env vars [c] in + let bnc = B.inner env vars [nc] in + let leqc = B.isLeq bcs bc in + let leqnc = B.isLeq bcs bnc in + let () = + if tracewiden && !tracebwd then begin + Format.printf "Node + Node with bcs = %a // bc = %a // bnc = %a [%b/%b]@." B.print bcs B.print bc B.print bnc leqc leqnc + end in + if leqc + then (* c is redundant *) + aux (((c, nc), (true, true)) :: p) ls (t1, t2) leafcs cs + else if leqnc + then (* nc is redundant *) + aux (((c, nc), (false, true)) :: p) ls (t1, t2) leafcs cs + else (* c and nc are not redundant *) + merge (aux (((c, nc), (true, true)) :: p) ls (t1, t2) leafcs (c :: cs), + aux (((c, nc), (false, true)) :: p) ls (t1, t2) leafcs (nc :: cs)) cs + end else raise (Invalid_argument "widen:aux:") + end in - aux [] lbl (t1, t2) [] + aux [] lbl (t1, t2) [] [] in if !tracebwd then begin @@ -1650,7 +1712,29 @@ struct | _ -> Node((c,nc),l,r) in { domain = domain; tree = aux t.tree []; env = env; vars = vars } - let print fmt t = + (* Compress nodes where leaves are upper-bounded by something into a single leaf. *) + let compress_consts t = + match t.tree with + | Leaf _ -> t + | _ -> + let rec aux t cs = + match t with + | Bot | Leaf _ -> t + | Node((c,nc),l,r) -> + try + (* Compress both children *) + match aux l (c::cs),aux r (nc::cs) with + | Leaf f1,Leaf f2 when F.defined f1 && F.defined f2 -> begin + (* The two leaves are compatible, are they compressable? *) + match F.getCompressed cs c nc f1 f2 with + | Some l -> Leaf l (* Yes *) + | None -> raise(GetOut(Leaf f1,Leaf f2)) (* No *) + end + | l,r -> raise(GetOut(l,r)) + with GetOut(l,r) -> Node((c,nc),l,r) + in { t with tree=aux t.tree [] } + + let print fmt t = let domain = t.domain in let env = t.env in let vars = t.vars in diff --git a/domains/Domain.ml b/domains/Domain.ml index 1491ec4d..d6a3eba1 100644 --- a/domains/Domain.ml +++ b/domains/Domain.ml @@ -62,6 +62,8 @@ module type RANKING_FUNCTION = sig val compress : t -> t + val compress_consts : t -> t + val print : Format.formatter -> t -> unit val print_graphviz_dot : Format.formatter -> t -> unit diff --git a/domains/Functions.ml b/domains/Functions.ml index 7826385a..9620da78 100644 --- a/domains/Functions.ml +++ b/domains/Functions.ml @@ -35,6 +35,8 @@ module type FUNCTION = sig val isLeq : kind -> B.t -> f -> f -> bool + val getCompressed : Lincons1.t list -> Lincons1.t -> Lincons1.t -> f -> f -> f option + val join : kind -> B.t -> f -> f -> f val learn: B.t -> f -> f -> f (* conflict-driven analysis *) val widen : ?jokers:int -> B.t -> f -> f -> f diff --git a/domains/Ordinals.ml b/domains/Ordinals.ml index 3b3ca28d..f1ca6d00 100644 --- a/domains/Ordinals.ml +++ b/domains/Ordinals.ml @@ -77,6 +77,18 @@ module OrdinalValued (F : FUNCTION) : FUNCTION = struct with Exit -> false else F.isLeq k b f1 f2 + let getCompressed cs c nc (f1, ff1) (f2, ff2) = + match F.getCompressed cs c nc f1 f2 with + | None -> None + | Some f -> + let rec inner ff1 ff2 ff = match ff1, ff2 with + | [], [] -> Some( f, List.rev ff ) + | [], ff' | ff', [] -> Some( f, List.rev_append ff ff' ) + | f1 :: ff1, f2 :: ff2 -> match F.getCompressed cs c nc f1 f2 with + | None -> None + | Some f' -> inner ff1 ff2 (f' :: ff) + in inner ff1 ff2 [] + let join k b (f1, ff1) (f2, ff2) = let env = B.env b in let vars = B.vars b in diff --git a/main/TerminationIterator.ml b/main/TerminationIterator.ml index 01233364..c92dd6b5 100644 --- a/main/TerminationIterator.ml +++ b/main/TerminationIterator.ml @@ -110,7 +110,11 @@ module TerminationIterator (D : RANKING_FUNCTION) = struct if B.isLeq i' i then i else let i'' = - if n <= !joinfwd then i' else B.widen i (B.join i i') + if n <= !joinfwd then i' else ( + let j = B.join i i' in + if !tracefwd && not !minimal then + Format.fprintf !fmt "j: %a\n" B.print j ; + B.widen i j ) in if !tracefwd && not !minimal then Format.fprintf !fmt "i'': %a\n" B.print i'' ; @@ -145,25 +149,37 @@ module TerminationIterator (D : RANKING_FUNCTION) = struct (* Backward Iterator + Recursion *) - let rec bwdStm ?domain funcs env vars (p, r, flag) s = + let rec bwdStm ?domain fixed_structure funcs env vars (p, r, flag) s = match s with | A_label _ -> (p, r, flag) | A_return -> (D.zero ?domain env vars, r, flag) - | A_assign ((l, _), (e, _)) -> (D.bwdAssign ?domain p (l, e), r, flag) + | A_assign ((l, _), (e, _)) -> + let j = D.bwdAssign ?domain p (l, e) in + let j' = if fixed_structure then j else D.compress_consts j in + if !tracebwd && not !minimal then ( + Format.fprintf !fmt "j: %a\n" D.print j ; + if j <> j' then Format.fprintf !fmt "j': %a\n" D.print j' ) ; + (j', r, flag) | A_assert (b, _) -> (D.filter ?domain p b, r, flag) | A_if ((b, ba), s1, s2) -> - let p1, _, flag1 = bwdBlk funcs env vars (p, r, flag) s1 in + let p1, _, flag1 = bwdBlk fixed_structure funcs env vars (p, r, flag) s1 in let p1 = D.filter ?domain p1 b in - let p2, _, flag2 = bwdBlk funcs env vars (p, r, flag) s2 in + let p2, _, flag2 = bwdBlk fixed_structure funcs env vars (p, r, flag) s2 in let p2 = D.filter ?domain p2 (fst (negBExp (b, ba))) in + let j = D.join APPROXIMATION p1 p2 in + let j' = if fixed_structure then j else D.compress_consts j in if !tracebwd && not !minimal then ( Format.fprintf !fmt "p1: %a\n" D.print p1 ; - Format.fprintf !fmt "p2: %a\n" D.print p2 ) ; - (D.join APPROXIMATION p1 p2, r, flag1 || flag2) + Format.fprintf !fmt "p2: %a\n" D.print p2 ; + Format.fprintf !fmt "j: %a\n" D.print j ; + if j <> j' then Format.fprintf !fmt "j': %a\n" D.print j' ) ; + (j', r, flag1 || flag2) | A_while (l, (b, ba), s) -> let a = InvMap.find l !fwdInvMap in let dm = if !refine then Some a else None in let p1 = D.filter ?domain:dm p (fst (negBExp (b, ba))) in + let old_fixed_structure = fixed_structure in + let fixed_structure = true in let rec aux (i, _, _) (p2, _, flag2) n = if !abort then raise Abort else @@ -189,7 +205,7 @@ module TerminationIterator (D : RANKING_FUNCTION) = struct in if !tracebwd && not !minimal then Format.fprintf !fmt "i'': %a\n" D.print i'' ; - let p2, _, flag2 = bwdBlk funcs env vars (i'', r, flag2) s in + let p2, _, flag2 = bwdBlk fixed_structure funcs env vars (i'', r, flag2) s in let p2' = D.filter ?domain:dm p2 b in aux (i'', r, flag2) (p2', r, flag2) (n + 1) ) else @@ -199,38 +215,45 @@ module TerminationIterator (D : RANKING_FUNCTION) = struct in if !tracebwd && not !minimal then Format.fprintf !fmt "i'': %a\n" D.print i'' ; - let p2, _, flag2 = bwdBlk funcs env vars (i'', r, flag2) s in + let p2, _, flag2 = bwdBlk fixed_structure funcs env vars (i'', r, flag2) s in let p2' = D.filter ?domain:dm p2 b in aux (i'', r, flag2) (p2', r, flag2) (n + 1) in let i = (D.bot ?domain:dm env vars, r, flag) in - let p2, _, flag2 = bwdBlk funcs env vars i s in + let p2, _, flag2 = bwdBlk fixed_structure funcs env vars i s in let p2' = D.filter ?domain:dm p2 b in let p, r, flag = aux i (p2', r, flag2) 1 in addBwdInv l p ; - if !refine then (D.refine p a, r, flag) else (p, r, flag) + let p = if !refine then D.refine p a else p in + let fixed_structure = old_fixed_structure in + let p' = if fixed_structure then p else D.compress_consts p in + if !tracebwd && not !minimal then ( + Format.fprintf !fmt "### %a:DONE ###:\n" label_print l ; + Format.fprintf !fmt "p: %a\n" D.print p ; + if p <> p' then Format.fprintf !fmt "p': %a\n" D.print p' ) ; + (p', r, flag) | A_call (f, ss) -> let f = StringMap.find f funcs in let p = bwdRec funcs env vars p f.funcBody in List.fold_left (fun (ap, ar, aflag) (s, _) -> - bwdStm ?domain funcs env vars (ap, ar, aflag) s ) + bwdStm ?domain fixed_structure funcs env vars (ap, ar, aflag) s ) (p, r, flag) ss | A_recall (f, ss) -> ( match domain with | None -> List.fold_left (fun (ap, ar, aflag) (s, _) -> - bwdStm funcs env vars (ap, ar, aflag) s ) + bwdStm fixed_structure funcs env vars (ap, ar, aflag) s ) (D.join APPROXIMATION p r, r, true) ss | Some domain -> List.fold_left (fun (ap, ar, aflag) (s, _) -> - bwdStm ~domain funcs env vars (ap, ar, aflag) s ) + bwdStm ~domain fixed_structure funcs env vars (ap, ar, aflag) s ) (r, r, true) ss ) - and bwdBlk funcs env vars (p, r, flag) (b : block) : D.t * D.t * bool = + and bwdBlk fixed_structure funcs env vars (p, r, flag) (b : block) : D.t * D.t * bool = let result_print l p = Format.fprintf !fmt "### %a ###:\n%a@." label_print l D.print p in @@ -245,11 +268,11 @@ module TerminationIterator (D : RANKING_FUNCTION) = struct stop := Sys.time () ; if !stop -. !start > !timeout then raise Timeout else - let b, rb, flagb = bwdBlk funcs env vars (p, r, flag) b in + let b, rb, flagb = bwdBlk fixed_structure funcs env vars (p, r, flag) b in let a = InvMap.find l !fwdInvMap in let p, r, flag = - if !refine then bwdStm ~domain:a funcs env vars (b, rb, flagb) s - else bwdStm funcs env vars (b, rb, flagb) s + if !refine then bwdStm ~domain:a fixed_structure funcs env vars (b, rb, flagb) s + else bwdStm fixed_structure funcs env vars (b, rb, flagb) s in let p = if !refine then D.refine p a else p in if !tracebwd && not !minimal then result_print l p ; @@ -257,7 +280,7 @@ module TerminationIterator (D : RANKING_FUNCTION) = struct (p, r, flag) and bwdRec funcs env vars (p : D.t) (b : block) : D.t = - let res, _, _ = bwdBlk funcs env vars (p, D.bot env vars, false) b in + let res, _, _ = bwdBlk false funcs env vars (p, D.bot env vars, false) b in res (* NOTE: unsound *) @@ -409,7 +432,6 @@ module TerminationIterator (D : RANKING_FUNCTION) = struct aux (B.top env vars) (D.bot env vars) 1 let analyze (vars, stmts, funcs) main robust = - let sv = vars in let rec aux xs env = match xs with | [] -> env diff --git a/run_tests.sh b/run_tests.sh new file mode 100755 index 00000000..e8f00940 --- /dev/null +++ b/run_tests.sh @@ -0,0 +1,151 @@ +#!/bin/bash + +shopt -s extglob + +execname="./main.exe" +in_file="tests.ref" +tab=$'\t' + +tottests=0 +totf=0 +nsucc=0 +nokf=0 + +# Colors +redcolor=$'\e[1;31m' +lightredcolor=$'\e[91m' +lightgreencolor=$'\e[92m' +greycolor=$'\e[2m' +resetcolor=$'\e[m' + +progress() { + if (( $1 == 0 )) + then + printf $'\e[G\e[K' # WARNING: Erase in Line + elif (( $1 == 1 )) + then + printf $'\e[GPhase 1: scanning file %d, test %d...' $totf $tottests + else + printf $'\e[GPhase %d: file %'"${#totf}"$'d/%d, test %'"${#tottests}"$'d/%d (%d %%)... (Time remaining: %02d:%02d)' $1 $2 $totf $3 $tottests $(( $3 * 100 / tottests )) $(( $4 / 60 )) $(( $4 % 60 )) + fi +} + +# First pass: count the number of tests etc +maximum=0 +while IFS= read -r line +do + f="${line%% *}" + [[ -z "$f" ]] && continue + [[ -f "$f" ]] || continue + + : $(( ++totf )) + ntests=0 + + line="${line/#+([^ ]) }" + while [[ "$line" =~ ^[^$tab]+"$tab"[[:digit:]]+"$tab"[^$tab]*"$tab" ]] + do + : $(( ++ntests )) + timeout="${line%% *}" + line="${line##+([^ ]) +([^ ]) *([^ ]) *([^ ])?( )}" + if [[ "$timeout" =~ ^[0-9]+s$ ]] + then + : $(( maximum += ${timeout%s} )) + elif [[ "$timeout" =~ ^[0-9]+m$ ]] + then + : $(( maximum += 60 * ${timeout%m} )) + else + progress 0 + echo "${redcolor}Error in reference:${resetcolor} file '$f' has invalid or unknown timeout value: {$timeout}" + fi + done + if [[ ! -z "$line" ]] + then + progress 0 + echo "${redcolor}Error in reference:${resetcolor} file '$f' has trailing text on the line: {$line}" + fi + + if [[ $ntests -eq 0 ]] + then + progress 0 + echo "${redcolor}Error in reference:${resetcolor} file '$f' has no test" + fi + : $(( tottests += ntests )) + progress 1 +done <"$in_file" + +ntest=0 +nf=0 +while IFS= read -r line +do + f="${line%% *}" + [[ -z "$f" ]] && continue + [[ -f "$f" ]] || continue + + : $(( ++nf )) + ntests=0 + noks=0 + errs="" + + line="${line/#+([^ ]) }" + while [[ "$line" =~ ^[^$tab]+"$tab"[[:digit:]]+"$tab"[^$tab]*"$tab" ]] + do + progress 2 $nf $(( ++ntest )) $maximum + : $(( ++ntests )) + timeout="${line%% *}" + line="${line##+([^ ]) }" + expcode="${line%% *}" + line="${line##+([^ ]) }" + expout="${line%% *}" + line="${line##*([^ ]) }" + params="${line%% *}" + line="${line##*([^ ])?( )}" + + output=$(timeout --foreground "$timeout" "$execname" $params "$f" 2>&1) + errcode=$? + + if (( errcode != expcode )) + then + errs="$errs${greycolor}[${resetcolor}$params${greycolor}] ${resetcolor}${lightredcolor}Unexpected return code:${resetcolor}${greycolor} expected ${resetcolor}${lightgreencolor}$expcode${resetcolor}${greycolor}" + if (( expcode == 0 )) + then + errs="$errs ($expout)" + fi + errs="$errs, got ${resetcolor}${lightredcolor}$errcode${resetcolor}"$'\n' + elif (( errcode == 0 )) && [[ $(echo -- "$output" | grep "Analysis Result: " | cut -d' ' -s -f3-) != "$expout" ]] + then + errs="$errs${greycolor}[${resetcolor}$params${greycolor}] ${resetcolor}${lightredcolor}Unexpected return message:${resetcolor}${greycolor} expected ${resetcolor}${lightgreencolor}$expout${resetcolor}${greycolor}, got ${resetcolor}${lightredcolor}$(echo -- "$output" | grep "Analysis Result: " | cut -d' ' -s -f3-)${resetcolor}"$'\n' + else + : $(( ++noks )) + fi + + if [[ "$timeout" =~ ^[0-9]+s$ ]] + then + : $(( maximum -= ${timeout%s} )) + elif [[ "$timeout" =~ ^[0-9]+m$ ]] + then + : $(( maximum -= 60 * ${timeout%m} )) + else + progress 0 + echo "${redcolor}Error in reference:${resetcolor} file '$f' has invalid or unknown timeout value: {$timeout}" + fi + done + if [[ ! -z "$errs" ]] + then + progress 0 + echo "${redcolor}Error on $f:${resetcolor}"$'\n'"$errs" + fi + + : $(( nsucc += noks )) + [[ $noks -eq $ntests ]] && : $(( ++nokf )) || true +done <"$in_file" + +progress 0 +if [[ $nsucc -eq $tottests ]] +then + echo "Result:" + echo "${greycolor}All tests (${resetcolor}${lightgreencolor}$tottests${resetcolor}${greycolor} over ${resetcolor}${lightgreencolor}$totf${resetcolor}${greycolor} files) ${resetcolor}${lightgreencolor}passed!${resetcolor}" +else + echo "Result:" + echo "${lightredcolor}$nokf${resetcolor}/${lightgreencolor}$totf${resetcolor}${greycolor} files passed (${resetcolor}$(( nokf * 100 / totf ))%${resetcolor}${greycolor})${resetcolor}" + echo "${greycolor}Passed ${resetcolor}${lightredcolor}$nsucc${resetcolor}/${lightgreencolor}$tottests${resetcolor}${greycolor} (${resetcolor}$(( nsucc * 100 / tottests ))%${greycolor}) tests${resetcolor}" +fi diff --git a/tests.ref b/tests.ref new file mode 100644 index 00000000..b34ade31 --- /dev/null +++ b/tests.ref @@ -0,0 +1,452 @@ + Comments are lines starting with a tab character. + Empty lines are also ignored. + + The format is the following: + {}+ + + Unknown + ------- + NOTE this seems slow with polyhedra + NOTE: what is this test? +tests/termination/mine.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 5s 0 UNKNOWN -termination -domain polyhedra + + Non-terminating + --------------- +tests/ctl/koskinen/acqrel_mod.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/koskinen/acqrel.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/koskinen/toylin1.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/koskinen/win4.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/cav2015.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/nestedRandomLoop_true-valid-ltl.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/PotentialMinimizeSEVPABug.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/simple-1.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/someNonterminating.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/timer-simple.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/togglecounter_true-valid-ltl.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/toggletoggle_true-valid-ltl.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/report/test_existential2.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/report/test_global.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/sv_comp/Bangalore_false-no-overflow.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/sv_comp/Ex02_false-termination_true-no-overflow.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/sv_comp/Ex07_false-termination_true-no-overflow.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/sv_comp/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/sv_comp/NO_02_false-termination_true-no-overflow.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/t2_cav13/P3.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/t2_cav13/P4.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/and_test.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/fin_ex.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/global_test_simple.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/or_test.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/potential_termination_1.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/until_existential.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: add guarantee testing +tests/guarantee/countdown.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/guarantee/mnav.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/guarantee/peterson.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/guarantee/simple.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/guarantee/sink.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/robust/sv_comp/witness/bin.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/robust/sv_comp/witness/sv_for1.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/AlternDivWide_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/AlternDivWidening_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/ChooseLife_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/ComplxStruc_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/DivWithoutMinus_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: check if this is not just a coincidence... +tests/sv_termination_restricted/DoubleNeg_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Et2_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Et4_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Ex08_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Factorial_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Fibonacci_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Flip_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Gauss_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/GCD_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 2s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/GCD2_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 6s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Lcm_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Loop_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Middle_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/MirrorInterv_false-termination.c 1s 0 UNKNOWN -termination 2s 0 UNKNOWN -termination -domain octagons 3s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/MirrorIntervSim_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: check if we can simplify the state on this test (it seems to do a loop unfolding) +tests/sv_termination_restricted/Narrowing_false-termination.c 1s 0 UNKNOWN -termination 3s 0 UNKNOWN -termination -domain octagons 3s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/NarrowKonv_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: this takes 30 seconds with the polyhedra domain?! Refining drops it to <1s +tests/sv_termination_restricted/NO_01_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/NO_02_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/NO_03_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/NO_04_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -refine -termination -domain polyhedra +tests/sv_termination_restricted/NO_10_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/NO_12_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/NO_13_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/NO_24_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/PastaC10_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/Swingers_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/UpAndDown_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/UpAndDownIneq_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/WhileNested_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination_restricted/WhileNestedOffset_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/2Nested_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Bangalore_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Bangalore_v2_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Bangalore_v3_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Hanoi_3vars_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Hanoi_plus_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Mysore_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/NonTermination2_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/NonTerminationSimple3_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/NonTerminationSimple4_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/NonTerminationSimple6_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Singapore_v1_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Singapore_v2_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/countdown.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/euclid.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/example0.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/example5.c 1s 0 UNKNOWN -termination -joinbwd 5 1s 0 UNKNOWN -termination -joinbwd 5 -domain octagons 1s 0 UNKNOWN -termination -joinbwd 5 -domain polyhedra +tests/termination/example7.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: the TERMINATION coment is wrong (take -2, 1, 2: we have a fixpoint) +tests/termination/issue8.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/sas2014a.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + What is smart widening? +tests/termination/sas2014c.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/tap2008a.c 1s 0 UNKNOWN 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/tap2008b.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/tap2008c.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/tap2008d.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/tap2008e.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/tap2008f.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/vmcai2004b.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/widening3.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/zune.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + + Terminating + ----------- +tests/ctl/ltl_automizer/Bug_NoLoopAtEndForTerminatingPrograms_safe.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/report/test_existential3.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/report/test_until.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/sv_comp/java_Sequence_true-termination_true-no-overflow.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/t2_cav13/P25.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/t2_cav13/P3_cheat.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 2s 0 TRUE -termination -domain octagons -ordinals 1 +tests/ctl/existential_test1.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/existential_test2.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/existential_test3.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/existential_test4.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/multi_branch_choice.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/next.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/until_test.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra + TODO: add guarantee testing +tests/guarantee/example.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra + NOTE: what? +tests/guarantee/pingpong.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/perso/continuous.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/perso/dummy.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/perso/interpolation.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/perso/isz1.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/perso/isz2.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/perso/my_sum.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/sv_comp/safe/sv_num4.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra + NOTE this seems slow + NOTE should also probably add a check for bug = 0 +tests/robust/sv_comp/safe/sv_num5.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/sv_comp/safe/sv_num6.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/sv_comp/witness/sv_num7.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/sv_comp/witness/sv_num8.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/robust/sv_comp/witness/sv_sum.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -refine +tests/termination/cacm2009a.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/cacm2009b.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -ordinals 1 -joinbwd 3 1s 0 TRUE -termination -ordinals 1 -joinbwd 3 -domain octagons 1s 0 TRUE -termination -ordinals 1 -joinbwd 3 -domain polyhedra +tests/sv_termination_restricted/a.01_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain octagons -ordinals 1 +tests/sv_termination_restricted/a.04_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/a.05_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/a.06_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/a.07_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/a.08_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/a.10_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.01_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.02_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.04_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.05_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.06_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.07_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.09_assume_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.09-no-inv_assume_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.10_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.11_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv_termination_restricted/b.12_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.13_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.14_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.15_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.16_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.17_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/b.18_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/c.02_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv_termination_restricted/c.03_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv_termination_restricted/c.07_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/c.08_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv_termination_restricted/easySum_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/ex1_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/flag_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/IntPath_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/java_Break_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/java_Continue1_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/java_Nested_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/java_Sequence_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/Log_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/MinusBuiltIn_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/MinusMin_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra + NOTE: constants compression breaks this test without -ordinals +tests/sv_termination_restricted/MinusUserDefined_true-termination.c 1s 0 TRUE -termination -ordinals 0 1s 0 TRUE -termination -domain octagons -ordinals 0 1s 0 TRUE -termination -domain polyhedra -ordinals 0 +tests/sv_termination_restricted/Nested_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaA1_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv_termination_restricted/PastaA4_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaA5_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaA6_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaA7_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaA8_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaA10_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaB1_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaB2_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaB4_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaB6_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaB7_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaB11_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv_termination_restricted/PastaB14_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaB15_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaB16_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaB17_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaC2_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv_termination_restricted/PastaC3_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv_termination_restricted/PastaC7_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination_restricted/PastaC9_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv_termination_restricted/Sequence_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv-termination-crafted/Bangalore_v4_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv-termination-crafted/Copenhagen_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv-termination-crafted/Copenhagen_disj_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/sv-termination-crafted/easy1_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv-termination-crafted/Hanoi_2vars_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Lobnya-Boolean-Reordered_true-termination.c 1s 0 TRUE -ordinals 1 -termination 1s 0 TRUE -ordinals 1 -termination -domain octagons 1s 0 TRUE -ordinals 1 -termination -domain polyhedra +tests/sv-termination-crafted/NonTermination4_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/NonTerminationSimple7_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Nyala-2lex_true-termination.c 1s 0 TRUE -ordinals 1 -termination 1s 0 TRUE -ordinals 1 -termination -domain octagons 1s 0 TRUE -ordinals 1 -termination -domain polyhedra +tests/sv-termination-crafted/Pure2Phase_true-termination.c 1s 0 TRUE -ordinals 2 -termination 1s 0 TRUE -ordinals 2 -termination -domain octagons 1s 0 TRUE -ordinals 2 -termination -domain polyhedra +tests/sv-termination-crafted/Rotation180_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/Singapore_plus_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/boolean.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/cda0.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/example1.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/example2.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/termination/example2a.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/example2b.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/example2c.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/example2d.c 1s 0 UNKNOWN -termination 2s 0 TRUE -termination -domain octagons 2s 0 TRUE -termination -domain polyhedra 1s 0 TRUE -termination -refine +tests/termination/example2e.c 2s 0 UNKNOWN -termination 3s 0 TRUE -termination -domain octagons 2s 0 TRUE -termination -domain polyhedra +tests/termination/example8.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -joinbwd 7 +tests/termination/example10.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -ordinals 2 -joinbwd 3 +tests/termination/postdecrement.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/postincrement.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/predecrement.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/preincrement.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/sas2010.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/sas2014b.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/sorting4.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/tacas2013a.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/tacas2013b.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/termination/tacas2013c.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 2s 0 TRUE -termination -joinbwd 3 -ordinals 1 + NOTE: why a jump to ~4s? +tests/termination/tacas2013d.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 2s 0 UNKNOWN -termination -domain polyhedra 5s 0 TRUE -termination -joinbwd 3 -ordinals 2 +tests/termination/vmcai2004a.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -joinbwd 5 +tests/termination/widening1.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 +tests/cacm2009c.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -refine -termination 1s 0 TRUE -refine -termination -domain octagons 1s 0 TRUE -refine -termination -domain polyhedra +tests/cacm2009d.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/example2a.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra + + Terminating but partially undetected + ------------------------------------ + TODO: why does this require '-ordinals 0' on octagons or more? +tests/ctl/t2_cav13/P26.c 1s 0 TRUE -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: check why the octagons domain cannot detect termination +tests/robust/sv_comp/witness/sv_num4f.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons -ordinals 0 1s 124 -termination -domain octagons -refine 1s 0 TRUE -termination -domain polyhedra -ordinals 0 1s 0 TRUE -termination -domain polyhedra -ordinals 0 -refine + TODO: check why the polyhedra domain only cannot detect termination +tests/robust/sv_comp/witness/sv_sum2.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 5s 0 UNKNOWN -termination -domain polyhedra + TODO: look from here + TODO: this fails with octagons +tests/sv_termination_restricted/a.09_assume_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra + TODO: check why the octagons domain cannot detect termination +tests/sv_termination_restricted/b.03_assume_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra + TODO: why not octagons+ordinals+refine or polyhedra+ordinals? +tests/sv_termination_restricted/b.03-no-inv_assume_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 -refine + TODO: check why the octagons domain cannot detect termination +tests/sv_termination_restricted/DivMinus_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra + TODO: check why the octagons domain cannot detect termination +tests/sv_termination_restricted/java_AG313_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra + TODO: check why the octagons domain cannot detect termination + This one seems quite short, look at it first? +tests/sv-termination-crafted/aaron2_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: x decreases every iteration since y > 0 +tests/sv-termination-crafted/Bangalore_true-termination.c 1s 0 UNKNOWN -ordinals 1 -termination 1s 0 UNKNOWN -ordinals 1 -termination -domain octagons 1s 0 UNKNOWN -ordinals 1 -termination -domain polyhedra + TODO check why this doesn't terminate either with the octagons domain(?) + NOTE: why refine? + W/ octagons, fractions appear in the fwd analysis (label 9: z *= -1) +tests/sv-termination-crafted/MenloPark_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -refine -ordinals 1 -termination -domain polyhedra + TODO: why are ordinals required? +tests/termination/widening2.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain polyhedra -ordinals 1 + + Terminating but undetected + -------------------------- + TODO: why is there a bottom? +tests/sv_termination/java_LogBuiltIn_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/sv_termination_restricted/c.01_assume_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? This one has no reason to, there is no conditional + TODO: why isn't this detected? +tests/sv_termination_restricted/c.01-no-inv_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/sv_termination_restricted/DivMinus2_true-termination.c 1s 0 UNKNOWN -termination 4s 0 UNKNOWN -termination -domain octagons 4s 0 UNKNOWN -termination -domain polyhedra + NOTE: I have no idea how to detect termination on this... +tests/sv_termination_restricted/Et1_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: y increases by at least 1 but this is undetected +tests/sv_termination_restricted/ex2_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + Same as with LogMult +tests/sv_termination_restricted/ex3a_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + Same as with LogMult +tests/sv_termination_restricted/ex3b_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why isn't this detected? +tests/sv_termination_restricted/fermat_true-termination.c 1s 0 UNKNOWN -termination 5s 0 UNKNOWN -termination -domain octagons 6s 0 UNKNOWN -termination -domain polyhedra + NOTE: same issue as PlusSwap +tests/sv_termination_restricted/Flip2_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: this takes 30 seconds with the polyhedra domain?! Refining drops it to <1s +tests/sv_termination_restricted/GCD3_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -refine -termination -domain polyhedra + TODO: why is there a top? +tests/sv_termination_restricted/GCD4_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 3s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/sv_termination_restricted/LogAG_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + This should be detected as y increases by at least 2 each loop iteration + NOTE: also the precondition is false, y must be at least 2 for the loop to terminate (but it's fine here) +tests/sv_termination_restricted/LogMult_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: a loop monovariant seems to be the pair (11c - x, -x) >= (-110, 110) with x0 <= 100 +tests/sv_termination_restricted/McCarthyIterative_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: this seems minimal + Same as B3? +tests/sv_termination_restricted/PastaA9_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/sv_termination_restricted/PastaB3_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + Same as with LogMult (but y increases by only 1) +tests/sv_termination_restricted/PastaC1_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: I have no idea how to detect termination on this... => joinbwd 4 +tests/sv_termination_restricted/PlusSwap_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: I have no idea how to detect termination on this... +tests/sv-termination-crafted/4NestedWith3Variables_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: phases +tests/sv-termination-crafted/2Nested_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: I have no idea how to detect termination on this... +tests/sv-termination-crafted/aaron3_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: I have no idea how to detect termination on this... + TODO: check why this doesn't terminate after 6m30 with the octagons domain (but the memory doesn't increase... infinite loop?) +tests/sv-termination-crafted/Benghazi_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: I have no idea how to detect termination on this... +tests/sv-termination-crafted/Benghazi_nondet_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: same as Stockholm_true-termination +tests/sv-termination-crafted/Gothenburg_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: same as Stockholm_true-termination +tests/sv-termination-crafted/Gothenburg_v2_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: McCarthy algorithm +tests/sv-termination-crafted/McCarthy91_Iteration_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: phases +tests/sv-termination-crafted/Mysore_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: check why this fails +tests/sv-termination-crafted/Parallel_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: I have no idea how to detect termination on this... +tests/sv-termination-crafted/Piecewise_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: phases +tests/sv-termination-crafted/Pure3Phase_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: x is strictly decreasing +tests/sv-termination-crafted/Singapore_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: this seems like an easy one (should be able to detect with the octagons domain, but fails to widen) +tests/sv-termination-crafted/Stockholm_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: min(x, y) is strictly decreasing every step +tests/sv-termination-crafted/TelAviv-Amir-Minimum_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: needs to do a loop unfolding +tests/sv-termination-crafted/Thun_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top?(?) +tests/sv-termination-crafted/Toulouse-BranchesToLoop_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/sv-termination-crafted/Toulouse-MultiBranchesToLoop_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE: this is due to the better adjacency algorithm +tests/termination/cav2006.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/termination/example1a.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/termination/example1b.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/termination/example1c.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why? +tests/termination/example1d.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/termination/example1e.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + TODO: why is there a top? +tests/termination/vijay.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + + Recursion, arrays, pointers and labels + --------- ------ -------- ------ +tests/ctl/koskinen/fig8-2007.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/ctl/koskinen/fig8-2007_mod.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_1_safe_sfty.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_2_safe_lifeness.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_3_safe_sfty.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_4_safe_sfty.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_5_safe_cheat.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_5_safe_sfty.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_6_safe_sfty.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_1_unsafe_sfty.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_2_unsafe_lifeness.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_3_unsafe_sfty.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_4_unsafe_sfty.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_5_unsafe_sfty.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/coolant_basis_6_unsafe_sfty.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/simple-2.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/ctl/ltl_automizer/timer-intermediate.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv_termination/Ackermann01_true-termination.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv_termination/Addition01_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination/Avg_true_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination/Binomial_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination/Et1_true_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination/Et2_true_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination/Et3_true_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination/Et4_true_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination/EvenOdd01_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination/Fibonacci01_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination/gcd01_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination/LeUserDefRec_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination/LogRecursive_true-termination.c 1s 0 TRUE -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination/MultCommutative_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination/Parts_true-termination.c 1s 0 UNKNOWN -termination 1s 0 TRUE -termination -domain octagons 1s 0 TRUE -termination -domain polyhedra +tests/sv_termination/rec_counter1_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination/rec_counter3_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination/recHanoi02_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination/TerminatorRec02_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv_termination/twisted_true-termination.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv_termination/TwoWay_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + NOTE octagons are slower than polyhedra (by ~1.5s) +tests/sv-termination-crafted/4BitCounterPointer_true-termination.c 1s 0 TRUE -termination 4s 0 TRUE -termination -domain octagons 3s 0 TRUE -termination -domain polyhedra +tests/sv-termination-crafted/Ackermann_false-termination.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv-termination-crafted/Ackermann_true-termination.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv-termination-crafted/Arrays01-EquivalentConstantIndices_true-termination.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv-termination-crafted/Arrays02-EquivalentConstantIndices_false-termination.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv-termination-crafted/Arrays03-ValueRestictsIndex_true-termination.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv-termination-crafted/Binary_Search_false-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/LexIndexValue-Array_true-termination.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv-termination-crafted/LexIndexValue-Pointer_false-valid-deref.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv-termination-crafted/LexIndexValue-Pointer_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/sv-termination-crafted/NonTermination3_false-termination.c 1s 2 -termination 1s 2 -termination -domain octagons 1s 2 -termination -domain polyhedra +tests/sv-termination-crafted/RecursiveMultiplication_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra +tests/termination/recursion.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra + + TODO: FIXME: + '-ordinals 1 -domain octagons' finishes fast and returns TRUE (normal) + '-domain octagons' finishes fast and returns UNKNOWN (normal) + '-refine -domain octagons' finishes SLOWLY (ABNORMAL) and returns UNKNOWN (normal) + '-refine -ordinals 1 -domain octagons' finishes SLOWLY (ABNORMAL) and returns UNKNOWN (ABNORMAL) + => '-refine' BREAKS THIS TEST with the octagons domain +tests/sv-termination-crafted/easy2_true-termination.c 1s 0 UNKNOWN -termination 1s 0 UNKNOWN -termination -domain octagons 1s 0 UNKNOWN -termination -domain polyhedra 1s 0 TRUE -termination -domain octagons -ordinals 1 1s 0 TRUE -termination -domain polyhedra -ordinals 1 + + TODO: FIXME: fails to terminate +tests/robust/sv_comp/safe/sv_lock2.c 1s 124 -termination 1s 124 -termination -domain octagons 1s 124 -termination -domain polyhedra