File tree 1 file changed +3
-3
lines changed
tests/regression/witness/int.t
1 file changed +3
-3
lines changed Original file line number Diff line number Diff line change 1
- $ goblint -- enable ana.sv-comp.functions --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.enums --enable ana.int.interval --enable ana.int.congruence --enable ana.int.interval_set --disable witness.invariant.split-conjunction int.c
1
+ $ goblint -- enable ana.sv-comp.functions --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.enums --enable ana.int.interval --enable ana.int.congruence --disable ana.int.interval_set --disable witness.invariant.split-conjunction int.c
2
2
[Success][Assert] Assertion " 1" will succeed (int.c:9 :5 - 9 :23 )
3
3
[Success][Assert] Assertion " 1" will succeed (int.c:12 :5 - 12 :23 )
4
4
[Success][Assert] Assertion " 1" will succeed (int.c:15 :5 - 15 :23 )
29
29
column: 5
30
30
function : main
31
31
location_invariant:
32
- string: ( 51 <= i && i <= 99 ) && ( 51 <= i && i <= 99 )
32
+ string: 51 <= i && i <= 99
33
33
type: assertion
34
34
format: C
35
35
- entry_type: location_invariant
40
40
column: 5
41
41
function : main
42
42
location_invariant:
43
- string: i <= 99 && i <= 99
43
+ string: i <= 99
44
44
type: assertion
45
45
format: C
You can’t perform that action at this time.
0 commit comments