Goose  Artifact [0148dc4e7e]

Artifact 0148dc4e7e0ce9a8eaf684528814abd5438e7c4d8e66ce37ccacf3642415f20c:

• File tests/g0/verification/z3gen/e-z3gen-test-4.txt — part of check-in [43f03d4856] at 2022-01-07 00:59:11 on branch trunk —
  • Verifier: fixed some errors in the implementation of the k-induction loop verification, which was breaking in some cases with nested loops
  • Verifier: fixed some data flow bugs that resulted in losing track of the state of some local variables in some situations
  (user: zlodo size: 2140)

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Checking compilation-time expression ===

=== Begin function verification trace ===
(=> b1 (= v0_1_65 p0))
(=> b1 (= v1_1_66 p1))
assume (distinct v0_1_65 v1_1_66)
(=> b1 (= v3_1_68 u67))
(=> b1 (= v3_1_69 v0_1_65))
(=> b1 (= v4_1_71 u70))
(=> b1 (= v4_1_72 v1_1_66))
(=> b1 (= v5_1_74 u73))
(=> b1 (= v5_1_75 v3_1_69))
(=> b1 (= v6_1_77 u76))
(=> b1 (= v6_1_78 v4_1_72))
(= e1_2 (and b1 (< v5_1_75 v6_1_78)))
(= b2 e1_2)
(=> b2 (= v8_2_80 u79))
(=> e1_2 (= v6_2_81 v6_1_78))
(=> b2 (= v6_2_82 v6_2_81))
(=> b2 (= v8_2_83 v6_2_82))
(=> b2 (= v9_2_85 u84))
(=> e1_2 (= v5_2_86 v5_1_75))
(=> b2 (= v5_2_87 v5_2_86))
(=> b2 (= v9_2_88 v5_2_87))
(=> b2 (= v5_2_89 v8_2_83))
(=> b2 (= v6_2_90 v9_2_88))
(= e1_3 (and b1 (not (< v5_1_75 v6_1_78))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v5_3_91 v5_1_75))
(=> e2_3 (= v5_3_91 v5_2_89))
(=> b3 (= v5_3_92 v5_3_91))
(=> e1_3 (= v6_3_93 v6_1_78))
(=> e2_3 (= v6_3_93 v6_2_90))
(=> b3 (= v6_3_94 v6_3_93))
check_unsat (and b3 (not (> (- v5_3_92 v6_3_94) 0)))
=== End function verification trace ===

=== Checking compilation-time expression ===

=== Begin function verification trace ===
(=> b1 (= v0_1_95 p0))
assume (distinct v0_1_95 0)
(=> b1 (= v0_1_97 v0_1_95))
(=> b1 (= v1_1_98 (* 2 v0_1_95)))
check_unsat (not (distinct v0_1_97 v1_1_98))
assume (> r96 0)
check_unsat (not (distinct r96 0))
=== End function verification trace ===

=== Checking compilation-time expression ===
(=> b1 (= v0_1_99 5))
check_unsat (not (distinct v0_1_99 0))

=== Begin function verification trace ===
=== End function verification trace ===