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

[variant baseline]
public fun Test::test_param($t0|_simple_R: Test::R, $t1|_ref_R: &Test::R, $t2|_simple_S: Test::S, $t3|_mut_R: &mut Test::R) {
  0: return ()
}

============ after pipeline `data_invariant_instrumentation` ================

[variant verification]
public fun Test::test_param($t0|_simple_R: Test::R, $t1|_ref_R: Test::R, $t2|_simple_S: Test::S, $t3|_mut_R: &mut Test::R) {
  0: assume And(WellFormed($t0), And(Gt(select Test::R.x($t0), select Test::S.y(select Test::R.s($t0))), Gt(select Test::S.y(select Test::R.s($t0)), 0)))
  1: assume And(WellFormed($t1), And(Gt(select Test::R.x($t1), select Test::S.y(select Test::R.s($t1))), Gt(select Test::S.y(select Test::R.s($t1)), 0)))
  2: assume And(WellFormed($t2), Gt(select Test::S.y($t2), 0))
  3: assume And(WellFormed($t3), And(Gt(select Test::R.x($t3), select Test::S.y(select Test::R.s($t3))), Gt(select Test::S.y(select Test::R.s($t3)), 0)))
  4: trace_local[_mut_R]($t3)
  5: label L1
  6: return ()
}