Concrete Playback=inplace produces unit test inside the harness

[jaisnan]

When I invoke concrete playback with Kani 0.28, the unit test is produced inside the harness instead of after it. Happens regardless of where the harness is placed (inside a module, outside of it).

using the following command line invocation:

kani /home/ubuntu/rectangle_example/src/main.rs --harness stretched_rectangle_can_hold_original --enable-unstable --concrete-playback=inplace

with Kani version: 0.28

I expected to see this happen: the unit test should be placed after the harness

    #[kani::proof]
    pub fn stretched_rectangle_can_hold_original() {
        let original = Rectangle {
            width: kani::any(),
            height: kani::any(),
        };
        let factor = kani::any();
        if let Some(larger) = original.stretch(factor) {
            assert!(larger.can_hold(&original));
        }
    }
    #[test]
    fn kani_concrete_playback_stretched_rectangle_can_hold_original_7840735556438970593() {
        let concrete_vals: Vec<Vec<u8>> = vec![
            // 0ul
            vec![0, 0, 0, 0, 0, 0, 0, 0],
            // 1ul
            vec![1, 0, 0, 0, 0, 0, 0, 0],
            // 9223372036854841360ul
            vec![16, 0, 1, 0, 0, 0, 0, 128],
        ];
        kani::concrete_playback_run(concrete_vals, stretched_rectangle_can_hold_original);
   }

Instead, this happened: the unit test was placed inside the harness

    #[kani::proof]
    pub fn stretched_rectangle_can_hold_original() {
      #[test]
      fn kani_concrete_playback_stretched_rectangle_can_hold_original_7840735556438970593() {
          let concrete_vals: Vec<Vec<u8>> = vec![
              // 0ul
              vec![0, 0, 0, 0, 0, 0, 0, 0],
              // 1ul
              vec![1, 0, 0, 0, 0, 0, 0, 0],
              // 9223372036854841360ul
              vec![16, 0, 1, 0, 0, 0, 0, 128],
          ];
          kani::concrete_playback_run(concrete_vals, stretched_rectangle_can_hold_original);
     }
        let original = Rectangle {
            width: kani::any(),
            height: kani::any(),
        };
        let factor = kani::any();
        if let Some(larger) = original.stretch(factor) {
            assert!(larger.can_hold(&original));
        }
    }

[jaisnan]

Note: Installed kani 0.27.0 and the issue disappeared.