diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index ab24515c28..55937a323d 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -680,19 +680,15 @@ struct let invariant t = let invariant m = - let earray = Lincons1.array_make t.env (Matrix.num_rows m) in - for i = 0 to Lincons1.array_length earray do + let one_constraint i = let row = Matrix.get_row m i in let coeff_vars = List.map (fun x -> Coeff.s_of_mpqf @@ Vector.nth row (Environment.dim_of_var t.env x), x) (vars t) in let cst = Coeff.s_of_mpqf @@ Vector.nth row (Vector.length row - 1) in - Lincons1.set_list (Lincons1.array_get earray i) coeff_vars (Some cst) - done; - let {lincons0_array; array_env}: Lincons1.earray = earray in - Array.enum lincons0_array - |> Enum.map (fun (lincons0: Lincons0.t) -> - Lincons1.{lincons0; env = array_env} - ) - |> List.of_enum + let e1 = Linexpr1.make t.env in + Linexpr1.set_list e1 coeff_vars (Some cst); + Lincons1.make e1 EQ + in + List.init (Matrix.num_rows m) one_constraint in BatOption.map_default invariant [] t.d diff --git a/tests/regression/63-affeq/19-witness.c b/tests/regression/63-affeq/19-witness.c new file mode 100644 index 0000000000..541aceab29 --- /dev/null +++ b/tests/regression/63-affeq/19-witness.c @@ -0,0 +1,34 @@ +//SKIP PARAM: --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none --set ana.relation.privatization top --enable witness.yaml.enabled +// Identical to Example 63/01; additionally checking that writing out witnesses does not crash the analyzer +#include + +void main(void) { + int i; + int j; + int k; + i = 2; + j = k + 5; + + while (i < 100) { + __goblint_check(3 * i - j + k == 1); + i = i + 1; + j = j + 3; + } + __goblint_check(3 * i - j + k == 1); + + // Represented with fractional coefficients and thus not put into witness yet + + int a = 0; + int b = 0; + int z = 0; + + while(z < 100) { + a++; + b += 2; + z++; + + __goblint_check(2*z - b == 0); + // b == 2*z is put into the witness + } + +}