[vasily@ionin C-playground]$ frama-c -slevel 10 -val puzzle.c
[kernel] Parsing puzzle.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva:alarm] puzzle.c:182: Warning:
  signed overflow. assert hash * 19 ≤ 2147483647;
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function board_hash:
  NON TERMINATING FUNCTION
[eva:final-states] Values at end of function board_hash_wrap:
  NON TERMINATING FUNCTION
[eva:final-states] Values at end of function init_board:
  __constr_expr_0.width ∈ {1}
                 .height ∈ {2}
                 .coordinates ∈ {0}
  __constr_expr_1{.width; .height} ∈ {2}
                 .coordinates.x ∈ {1}
                 .coordinates.y ∈ {0}
  __constr_expr_2.width ∈ {1}
                 .height ∈ {2}
                 .coordinates.x ∈ {3}
                 .coordinates.y ∈ {0}
  __constr_expr_3.width ∈ {1}
                 .height ∈ {2}
                 .coordinates.x ∈ {0}
                 .coordinates.y ∈ {2}
  __constr_expr_4.width ∈ {2}
                 {.height; .coordinates.x} ∈ {1}
                 .coordinates.y ∈ {2}
  __constr_expr_5.width ∈ {1}
                 .height ∈ {2}
                 .coordinates.x ∈ {3}
                 .coordinates.y ∈ {2}
  __constr_expr_6{.width; .height; .coordinates.x} ∈ {1}
                 .coordinates.y ∈ {3}
  __constr_expr_7{.width; .height} ∈ {1}
                 .coordinates.x ∈ {2}
                 .coordinates.y ∈ {3}
  __constr_expr_8{.width; .height} ∈ {1}
                 .coordinates.x ∈ {0}
                 .coordinates.y ∈ {4}
  __constr_expr_9{.width; .height} ∈ {1}
                 .coordinates.x ∈ {3}
                 .coordinates.y ∈ {4}
  __constr_expr_10.x ∈ {1}
                  .y ∈ {4}
  __constr_expr_11.x ∈ {2}
                  .y ∈ {4}
  b.width ∈ {4}
   .height ∈ {5}
   .free_p1.x ∈ {1}
   .free_p1.y ∈ {4}
   .free_p2.x ∈ {2}
   .free_p2.y ∈ {4}
   .chips[0].width ∈ {1}
   .chips[0].height ∈ {2}
   .chips[0].coordinates ∈ {0}
   .chips[1]{.width; .height} ∈ {2}
   .chips[1].coordinates.x ∈ {1}
   .chips[1].coordinates.y ∈ {0}
   .chips[2].width ∈ {1}
   .chips[2].height ∈ {2}
   .chips[2].coordinates.x ∈ {3}
   .chips[2].coordinates.y ∈ {0}
   .chips[3].width ∈ {1}
   .chips[3].height ∈ {2}
   .chips[3].coordinates.x ∈ {0}
   .chips{[3].coordinates.y; [4].width} ∈ {2}
   .chips[4]{.height; .coordinates.x} ∈ {1}
   .chips[4].coordinates.y ∈ {2}
   .chips[5].width ∈ {1}
   .chips[5].height ∈ {2}
   .chips[5].coordinates.x ∈ {3}
   .chips[5].coordinates.y ∈ {2}
   .chips[6]{.width; .height; .coordinates.x} ∈ {1}
   .chips[6].coordinates.y ∈ {3}
   .chips[7]{.width; .height} ∈ {1}
   .chips[7].coordinates.x ∈ {2}
   .chips[7].coordinates.y ∈ {3}
   .chips[8]{.width; .height} ∈ {1}
   .chips[8].coordinates.x ∈ {0}
   .chips[8].coordinates.y ∈ {4}
   .chips[9]{.width; .height} ∈ {1}
   .chips[9].coordinates.x ∈ {3}
   .chips[9].coordinates.y ∈ {4}
[eva:final-states] Values at end of function solve:
  NON TERMINATING FUNCTION
[eva:final-states] Values at end of function solve_wrap:
  NON TERMINATING FUNCTION
[eva:final-states] Values at end of function main:
  NON TERMINATING FUNCTION