============ initial translation from Move ================

[variant baseline]
fun TestSpecBlock::looping($t0|x: u64): u64 {
     var $t1: u64
     var $t2: u64
     var $t3: bool
     var $t4: u64
     var $t5: u64
     var $t6: u64
     var $t7: u64
  0: assume Le($t0, 10)
  1: goto 2
  2: label L3
  3: $t1 := copy($t0)
  4: $t2 := 10
  5: $t3 := <($t1, $t2)
  6: if ($t3) goto 7 else goto 14
  7: label L0
  8: assume Lt($t0, 10)
  9: $t4 := move($t0)
 10: $t5 := 1
 11: $t6 := +($t4, $t5)
 12: $t0 := $t6
 13: goto 2
 14: label L2
 15: assert Eq<u64>($t0, 10)
 16: $t7 := move($t0)
 17: return $t7
}


[variant baseline]
fun TestSpecBlock::simple1($t0|x: u64, $t1|y: u64) {
     var $t2: u64
     var $t3: u64
     var $t4: bool
     var $t5: bool
     var $t6: u64
  0: $t2 := copy($t0)
  1: $t3 := copy($t1)
  2: $t4 := >($t2, $t3)
  3: $t5 := !($t4)
  4: if ($t5) goto 5 else goto 8
  5: label L0
  6: $t6 := 1
  7: abort($t6)
  8: label L2
  9: assert Gt($t0, $t1)
 10: return ()
}


[variant baseline]
fun TestSpecBlock::simple2($t0|x: u64) {
     var $t1|y: u64
     var $t2: u64
     var $t3: u64
     var $t4: u64
  0: $t2 := copy($t0)
  1: $t3 := 1
  2: $t4 := +($t2, $t3)
  3: $t1 := $t4
  4: assert Eq<u64>($t0, Sub($t1, 1))
  5: return ()
}


[variant baseline]
fun TestSpecBlock::simple3($t0|x: u64, $t1|y: u64) {
  0: assume Gt($t0, $t1)
  1: assert Ge($t0, $t1)
  2: return ()
}


[variant baseline]
fun TestSpecBlock::simple4($t0|x: u64, $t1|y: u64) {
     var $t2|z: u64
     var $t3: u64
     var $t4: u64
     var $t5: u64
  0: $t3 := copy($t0)
  1: $t4 := copy($t1)
  2: $t5 := +($t3, $t4)
  3: $t2 := $t5
  4: assume Gt($t0, $t1)
  5: assert Gt($t2, Mul(2, $t1))
  6: return ()
}