/mnt/thread-witnesses/replication/bench/thread-witnesses/st-cross/../../../ourtool/goblint --conf conf/svcomp-yaml-validate.json --enable dbg.timing.enabled --set 'ana.activated[+]' apron --set ana.apron.domain polyhedra --witness.yaml.unassume cpachecker/dijkstra-u_valuebound100.yml.witness.yml --witness.yaml.validate cpachecker/dijkstra-u_valuebound100.yml.witness.yml --sets ana.specification ../properties/unreach-call.prp --sets exp.architecture 32bit ../plain/dijkstra-u_valuebound100.c


--------------------------------------------------------------------------------


--sets is deprecated, use --set instead.
--sets is deprecated, use --set instead.
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Warning][Witness] couldn't locate invariant: (q == (1U) && h == (13U) && p == (7U)) || (q == (1U) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && h == (9U) && p == (5U)) || (q == (1U) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && h == (21U) && p == (10U)) || (q == (1U) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && h == (1U) && p == (1U)) || (q == (1U) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && h == (0U) && p == (0U)) || (q == (1U) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U)))) && h == (17U) && p == (8U)) || (q == (1U) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && h == (5U) && p == (2U)) || (q == (1U) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U)))) && !(p == (8U)) && (!(h == (5U)) || (h == (5U) && !(p == (2U)))) && h == (17U) && p == (9U)) || (q == (1U) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && !(p == (2U)) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && h == (5U) && p == (3U)) || (q == (1U) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && !(p == (5U)) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (5U)) || (h == (5U) && !(p == (2U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (5U)) || (h == (5U) && !(p == (3U)))) && h == (9U) && p == (4U)) || (q == (1U) && !(p == (7U)) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (5U)) || (h == (5U) && !(p == (2U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (5U)) || (h == (5U) && !(p == (3U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && h == (13U) && p == (6U)) (../plain/dijkstra-u_valuebound100.c:47:13)
[Warning][Witness] couldn't locate invariant: (h == (17U) && p == (9U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U)))) && h == (0U) && p == (0U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && h == (0U) && p == (0U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && h == (4U) && p == (4U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && h == (80U) && p == (32U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && h == (20U) && p == (12U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && h == (13U) && p == (7U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && h == (0U) && p == (0U) && q == (256U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && h == (1U) && p == (1U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && !(p == (7U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && h == (13U) && p == (6U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && h == (9U) && p == (4U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && h == (0U) && p == (0U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && !(p == (12U)) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && h == (20U) && p == (8U) && q == (4U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && h == (36U) && p == (16U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && !(p == (9U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && h == (17U) && p == (8U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && h == (64U) && p == (64U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && !(q == (64U)) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U))) && h == (0U) && p == (0U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && !(p == (4U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && h == (9U) && p == (5U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && !(p == (16U)) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && h == (36U) && p == (20U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && h == (16U) && p == (16U) && q == (16U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && h == (5U) && p == (3U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && (!(h == (5U)) || (h == (5U) && !(p == (3U)))) && h == (21U) && p == (10U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && !(p == (3U)) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && h == (5U) && p == (2U) && q == (1U)) (../plain/dijkstra-u_valuebound100.c:44:9)
[Warning][Witness] couldn't locate invariant: (h == (17U) && p == (9U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U)))) && h == (0U) && p == (0U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && h == (0U) && p == (0U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && h == (4U) && p == (4U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && h == (80U) && p == (32U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && h == (20U) && p == (12U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && h == (13U) && p == (7U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && h == (0U) && p == (0U) && q == (256U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && h == (1U) && p == (1U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && !(p == (7U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && h == (13U) && p == (6U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && h == (9U) && p == (4U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && h == (0U) && p == (0U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && !(p == (12U)) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && h == (20U) && p == (8U) && q == (4U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && h == (36U) && p == (16U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && !(p == (9U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && h == (17U) && p == (8U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && h == (64U) && p == (64U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && !(q == (64U)) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U))) && h == (0U) && p == (0U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && !(p == (4U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && h == (9U) && p == (5U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && !(p == (16U)) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && h == (36U) && p == (20U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && h == (16U) && p == (16U) && q == (16U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && h == (5U) && p == (3U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && (!(h == (5U)) || (h == (5U) && !(p == (3U)))) && h == (21U) && p == (10U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && !(p == (3U)) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && h == (5U) && p == (2U) && q == (1U)) (../plain/dijkstra-u_valuebound100.c:43:9)
[Warning][Witness] couldn't locate invariant: (h == (17U) && p == (9U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U)))) && h == (0U) && p == (0U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && h == (0U) && p == (0U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && h == (4U) && p == (4U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && h == (80U) && p == (32U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && h == (20U) && p == (12U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && h == (13U) && p == (7U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && h == (0U) && p == (0U) && q == (256U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && h == (1U) && p == (1U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && !(p == (7U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && h == (13U) && p == (6U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && h == (9U) && p == (4U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && h == (0U) && p == (0U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && !(p == (12U)) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && h == (20U) && p == (8U) && q == (4U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && h == (36U) && p == (16U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && !(p == (9U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && h == (17U) && p == (8U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && h == (64U) && p == (64U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && !(q == (64U)) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U))) && h == (0U) && p == (0U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && !(p == (4U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && h == (9U) && p == (5U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && !(p == (16U)) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && h == (36U) && p == (20U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && h == (16U) && p == (16U) && q == (16U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && h == (5U) && p == (3U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && (!(h == (5U)) || (h == (5U) && !(p == (3U)))) && h == (21U) && p == (10U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && !(p == (3U)) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && h == (5U) && p == (2U) && q == (1U)) (../plain/dijkstra-u_valuebound100.c:41:9)
[Warning][Witness] couldn't locate invariant: (h == (64U) && p == (0U) && q == (64U)) || ((!(h == (64U)) || (h == (64U) && !(p == (0U))) || (h == (64U) && p == (0U) && !(q == (64U)))) && h == (80U) && p == (32U) && q == (16U)) || ((!(h == (64U)) || (h == (64U) && !(p == (0U))) || (h == (64U) && p == (0U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && h == (20U) && p == (8U) && q == (4U)) || ((!(h == (64U)) || (h == (64U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && h == (1U) && p == (0U) && q == (1U)) || ((!(h == (64U)) || (h == (64U) && !(p == (0U))) || (h == (64U) && p == (0U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(q == (4U)))) && (!(h == (1U)) || (h == (1U) && !(p == (0U)))) && h == (17U) && p == (8U) && q == (1U)) || ((!(h == (64U)) || (h == (64U) && !(p == (0U))) || (h == (64U) && p == (0U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (1U)) || (h == (1U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && h == (9U) && p == (4U) && q == (1U)) || ((!(h == (64U)) || (h == (64U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && (!(h == (1U)) || (h == (1U) && !(q == (1U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && h == (4U) && p == (0U) && q == (4U)) || ((!(h == (64U)) || (h == (64U) && !(p == (0U))) || (h == (64U) && p == (0U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (1U)) || (h == (1U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (4U)) || (h == (4U) && !(p == (0U))) || (h == (4U) && p == (0U) && !(q == (4U)))) && h == (5U) && p == (2U) && q == (1U)) || ((!(h == (64U)) || (h == (64U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (1U)) || (h == (1U) && !(q == (1U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(q == (4U)))) && (!(h == (5U)) || (h == (5U) && !(p == (2U))) || (h == (5U) && p == (2U) && !(q == (1U)))) && h == (16U) && p == (0U) && q == (16U)) || ((!(h == (64U)) || (h == (64U) && !(p == (0U))) || (h == (64U) && p == (0U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (1U)) || (h == (1U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (4U)) || (h == (4U) && !(p == (0U))) || (h == (4U) && p == (0U) && !(q == (4U)))) && (!(h == (5U)) || (h == (5U) && !(p == (2U)))) && (!(h == (16U)) || (h == (16U) && !(p == (0U))) || (h == (16U) && p == (0U) && !(q == (16U)))) && h == (13U) && p == (6U) && q == (1U)) || ((!(h == (64U)) || (h == (64U) && !(p == (0U))) || (h == (64U) && p == (0U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (1U)) || (h == (1U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (4U)) || (h == (4U) && !(p == (0U))) || (h == (4U) && p == (0U) && !(q == (4U)))) && (!(h == (5U)) || (h == (5U) && !(p == (2U)))) && (!(h == (16U)) || (h == (16U) && !(p == (0U))) || (h == (16U) && p == (0U) && !(q == (16U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && h == (21U) && p == (10U) && q == (1U)) || ((!(h == (64U)) || (h == (64U) && !(p == (0U))) || (h == (64U) && p == (0U) && !(q == (64U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && (!(h == (1U)) || (h == (1U) && !(p == (0U))) || (h == (1U) && p == (0U) && !(q == (1U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (0U)))) && (!(h == (5U)) || (h == (5U) && !(p == (2U))) || (h == (5U) && p == (2U) && !(q == (1U)))) && (!(h == (16U)) || (h == (16U) && !(p == (0U))) || (h == (16U) && p == (0U) && !(q == (16U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (21U)) || (h == (21U) && !(p == (10U))) || (h == (21U) && p == (10U) && !(q == (1U)))) && h == (36U) && p == (16U) && q == (4U)) (../plain/dijkstra-u_valuebound100.c:49:9)
[Warning][Witness] couldn't locate invariant: (h == (17U) && p == (9U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U)))) && h == (0U) && p == (0U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && h == (0U) && p == (0U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && h == (4U) && p == (4U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && h == (80U) && p == (32U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && h == (20U) && p == (12U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && h == (13U) && p == (7U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && h == (0U) && p == (0U) && q == (256U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && h == (1U) && p == (1U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && !(p == (7U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && h == (13U) && p == (6U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && h == (9U) && p == (4U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && h == (0U) && p == (0U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && !(p == (12U)) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && h == (20U) && p == (8U) && q == (4U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && h == (36U) && p == (16U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && !(p == (9U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && h == (17U) && p == (8U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && h == (64U) && p == (64U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && !(q == (64U)) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U))) && h == (0U) && p == (0U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && !(p == (4U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && h == (9U) && p == (5U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && !(p == (16U)) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && h == (36U) && p == (20U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && h == (16U) && p == (16U) && q == (16U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && h == (5U) && p == (3U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && (!(h == (5U)) || (h == (5U) && !(p == (3U)))) && h == (21U) && p == (10U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && !(p == (3U)) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && h == (5U) && p == (2U) && q == (1U)) (../plain/dijkstra-u_valuebound100.c:40:9)
[Warning][Witness] couldn't locate invariant: (h == (17U) && p == (9U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U)))) && h == (0U) && p == (0U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && h == (0U) && p == (0U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && h == (4U) && p == (4U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && h == (80U) && p == (32U) && q == (16U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && h == (20U) && p == (12U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && h == (13U) && p == (7U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && h == (0U) && p == (0U) && q == (256U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && h == (1U) && p == (1U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && !(p == (7U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && h == (13U) && p == (6U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && h == (9U) && p == (4U) && q == (1U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && h == (0U) && p == (0U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && !(p == (12U)) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && h == (20U) && p == (8U) && q == (4U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && h == (36U) && p == (16U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && !(p == (9U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && h == (17U) && p == (8U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && h == (64U) && p == (64U) && q == (64U)) || ((!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U))) && !(q == (1U)) && !(q == (16U)) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U))) && !(q == (256U)) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U))) && !(q == (64U)) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U))) && h == (0U) && p == (0U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && !(p == (4U)) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && h == (9U) && p == (5U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U)))) && !(p == (16U)) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && h == (36U) && p == (20U) && q == (4U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U))) || (h == (17U) && p == (9U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (1U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U))) || (h == (13U) && p == (7U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U))) || (h == (1U) && p == (1U) && !(q == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U))) || (h == (13U) && p == (6U) && !(q == (1U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U))) || (h == (9U) && p == (4U) && !(q == (1U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U))) || (h == (17U) && p == (8U) && !(q == (1U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U))) || (h == (9U) && p == (5U) && !(q == (1U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && h == (16U) && p == (16U) && q == (16U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && h == (5U) && p == (3U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && (!(h == (5U)) || (h == (5U) && !(p == (3U)))) && h == (21U) && p == (10U) && q == (1U)) || ((!(h == (0U)) || (h == (0U) && !(p == (0U)))) && (!(h == (17U)) || (h == (17U) && !(p == (9U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (16U)))) && (!(h == (4U)) || (h == (4U) && !(p == (4U))) || (h == (4U) && p == (4U) && !(q == (4U)))) && (!(h == (80U)) || (h == (80U) && !(p == (32U))) || (h == (80U) && p == (32U) && !(q == (16U)))) && (!(h == (20U)) || (h == (20U) && !(p == (12U))) || (h == (20U) && p == (12U) && !(q == (4U)))) && (!(h == (13U)) || (h == (13U) && !(p == (7U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (256U)))) && (!(h == (1U)) || (h == (1U) && !(p == (1U)))) && (!(h == (13U)) || (h == (13U) && !(p == (6U)))) && (!(h == (9U)) || (h == (9U) && !(p == (4U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (64U)))) && (!(h == (20U)) || (h == (20U) && !(p == (8U))) || (h == (20U) && p == (8U) && !(q == (4U)))) && (!(h == (36U)) || (h == (36U) && !(p == (16U))) || (h == (36U) && p == (16U) && !(q == (4U)))) && (!(h == (17U)) || (h == (17U) && !(p == (8U)))) && (!(h == (64U)) || (h == (64U) && !(p == (64U))) || (h == (64U) && p == (64U) && !(q == (64U)))) && (!(h == (0U)) || (h == (0U) && !(p == (0U))) || (h == (0U) && p == (0U) && !(q == (4U)))) && (!(h == (9U)) || (h == (9U) && !(p == (5U)))) && (!(h == (36U)) || (h == (36U) && !(p == (20U))) || (h == (36U) && p == (20U) && !(q == (4U)))) && (!(h == (16U)) || (h == (16U) && !(p == (16U))) || (h == (16U) && p == (16U) && !(q == (16U)))) && !(p == (3U)) && (!(h == (21U)) || (h == (21U) && !(p == (10U)))) && h == (5U) && p == (2U) && q == (1U)) (../plain/dijkstra-u_valuebound100.c:42:9)

runtime: 00:00:10.105
vars: 92, evals: 595

|rho|=92
|called|=6
|stable|=78
|infl|=89
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=70
Found 11 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/dijkstra-u_valuebound100.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/dijkstra-u_valuebound100.c:5:1-5:76
2	contexts for entry state of assume_abort_if_not (2006) on ../plain/dijkstra-u_valuebound100.c:8:1-10:1
1	contexts for entry state of main (2012) on ../plain/dijkstra-u_valuebound100.c:19:1-61:1
1	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140

Memory statistics: total=2068.41MB, max=21.63MB, minor=2064.91MB, major=153.67MB, promoted=150.16MB
    minor collections=999  major collections=28 compactions=0


runtime: 00:00:20.124
vars: 92, evals: 1023

|rho|=92
|called|=6
|stable|=79
|infl|=89
|wpoint|=2
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=70
Found 11 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/dijkstra-u_valuebound100.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/dijkstra-u_valuebound100.c:5:1-5:76
2	contexts for entry state of assume_abort_if_not (2006) on ../plain/dijkstra-u_valuebound100.c:8:1-10:1
1	contexts for entry state of main (2012) on ../plain/dijkstra-u_valuebound100.c:19:1-61:1
1	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140

Memory statistics: total=3999.33MB, max=21.63MB, minor=3995.82MB, major=300.10MB, promoted=296.58MB
    minor collections=1930  major collections=50 compactions=0


runtime: 00:00:30.141
vars: 92, evals: 1444

|rho|=92
|called|=6
|stable|=92
|infl|=89
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=70
Found 11 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/dijkstra-u_valuebound100.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/dijkstra-u_valuebound100.c:5:1-5:76
2	contexts for entry state of assume_abort_if_not (2006) on ../plain/dijkstra-u_valuebound100.c:8:1-10:1
1	contexts for entry state of main (2012) on ../plain/dijkstra-u_valuebound100.c:19:1-61:1
1	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140

Memory statistics: total=5887.56MB, max=21.63MB, minor=5884.03MB, major=441.15MB, promoted=437.62MB
    minor collections=2841  major collections=71 compactions=0


runtime: 00:00:40.179
vars: 92, evals: 1852

|rho|=92
|called|=6
|stable|=92
|infl|=89
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=70
Found 11 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/dijkstra-u_valuebound100.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/dijkstra-u_valuebound100.c:5:1-5:76
2	contexts for entry state of assume_abort_if_not (2006) on ../plain/dijkstra-u_valuebound100.c:8:1-10:1
1	contexts for entry state of main (2012) on ../plain/dijkstra-u_valuebound100.c:19:1-61:1
1	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140

Memory statistics: total=7733.83MB, max=21.63MB, minor=7730.29MB, major=582.14MB, promoted=578.60MB
    minor collections=3733  major collections=93 compactions=0


runtime: 00:00:50.169
vars: 92, evals: 2261

|rho|=92
|called|=6
|stable|=79
|infl|=89
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=70
Found 11 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/dijkstra-u_valuebound100.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/dijkstra-u_valuebound100.c:5:1-5:76
2	contexts for entry state of assume_abort_if_not (2006) on ../plain/dijkstra-u_valuebound100.c:8:1-10:1
1	contexts for entry state of main (2012) on ../plain/dijkstra-u_valuebound100.c:19:1-61:1
1	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140

Memory statistics: total=9612.01MB, max=21.63MB, minor=9608.45MB, major=723.09MB, promoted=719.54MB
    minor collections=4639  major collections=114 compactions=0


runtime: 00:01:00.186
vars: 92, evals: 2669

|rho|=92
|called|=6
|stable|=79
|infl|=89
|wpoint|=3
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=70
Found 11 contexts for 5 functions. Top 5 functions:
5	contexts for entry state of __VERIFIER_assert (2009) on ../plain/dijkstra-u_valuebound100.c:11:1-17:1
2	contexts for entry state of reach_error (1999) on ../plain/dijkstra-u_valuebound100.c:5:1-5:76
2	contexts for entry state of assume_abort_if_not (2006) on ../plain/dijkstra-u_valuebound100.c:8:1-10:1
1	contexts for entry state of main (2012) on ../plain/dijkstra-u_valuebound100.c:19:1-61:1
1	contexts for entry state of __VERIFIER_nondet_uint (374) on /mnt/thread-witnesses/replication/ourtool/lib/sv-comp/stub/src/sv-comp.c:43:70-43:140

Memory statistics: total=11443.77MB, max=21.63MB, minor=11440.21MB, major=861.36MB, promoted=857.80MB
    minor collections=5522  major collections=134 compactions=0

