-
Notifications
You must be signed in to change notification settings - Fork 0
ciobaca/rmt
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
To report problems If there is something that is not working or if you have questions on RMT, please contact me at: [email protected]. Prerequisites * A modern C++ compiler (a recent version of g++, clang or MSVC will do) * git * CMake * Z3 Compilation We list the exact steps for an Ubuntu machine. Please adapt for use on Mac or Windows. * Step 1: Install build-essential (g++) and cmake: sudo apt install build-essential cmake * Step 2: Clone the Z3 repository in ~/z3: git clone https://github.com/Z3Prover/z3.git * Step 3: Compile Z3 in ~/z3/build (4 parallel compilation processes): cd z3 mkdir build cd build cmake .. make -j 4 cd ../.. This step might take around 10 minutes, depending on your exact machine. * Step 4: Clone the RMT repository in ~/rmt: git clone https://github.com/ciobaca/rmt.git * Step 5: Build RMT (links against Z3, previously compiled) cd rmt mkdir build cd build cmake .. -DZ3_DIR=~/z3/build make -j 4 cd ../.. Step 6: running RMT: cd rmt/examples/ ~/rmt/build/rmt -v 0 example1.rmt This will will rmt with verbosity 0 (lowest) on the given example.
About
Rewriting Modulo Theories Tool
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published