• Rust 1.60.0-nightly: installation guide
• Rosette: installation guide
  • We used the Z3 backend in this project

• Make sure the program with property specifications is put under the directory ./spec_code/
• Run the tool with command:

cargo run [input.rs] [output.rs]

for example

cargo run example_unique.rs example_unique_output.rs

• The generated file will appear in the directory ./gen_code/