dreal3
dreal3 copied to clipboard
Specify `python2` instead of assuming default
Currently the script fails if your default python
is version 3, in this fashion:
(base) max@max-XPS-13-9310:~/tools/dreal3/dReal-3.16.06.02-linux/bin$ ./dReach -k 10 bouncing_ball.drh --verbose --precision 0.001 --visualize
File "<string>", line 1
import os,sys; print os.path.realpath("./dReach")
^
SyntaxError: invalid syntax
usage: ./dReach options <*.drh> <options to dReal>
dReach: Bounded Model Checking for for Nonlinear Hybrid Systems
OPTIONS:
-k <N> / -u <N> specify the upperbound of unrolling steps (default: 3)
-l <N> specify the lowerbound of unrolling steps (default: 0)
-b use BMC heuristic with disjunctive path encoding (default: do not use)
-r -b and filter unreachable modes from SMT encoding (default: do not use)
-e -r and filter continuous variables from SMT encoding (default: do not use)
-d disjunctive path encoding (default: do not use)
-z apply exit codes (default: do not use):
51 if SAT,
52 if UNSAT,
1 abnormal termination
-n parse new .drh file format (default: do not use)
-s parse new .drh file format and use synchronous encoding (default: do not use)
EXAMPLE:
dReach -k 10 bouncing_ball.drh --verbose --precision 0.001 --visualize
dReach -l 3 -u 10 bouncing_ball.drh --verbose --precision 0.001 --visualize
an easy fix is just to specify that you want to use version 2. On my system, and indeed on most systems, if you say python2
it'll use 2.7, which is probably what you intend.
Thanks for making contributions to dReal! Before opening a pull-request, please check the following things:
- [ ] Run
make
and check the code compiles. Please try both of gcc and clang. - [ ] Run
make format
to run clang-format over your contributions. - [ ] Run
make style
and check there is no style error. - [ ] Follow our Git commit message convention.
- [x] Ensure the PR description clearly describes the problem and solution. Include the relevant issue number if applicable.
- [ ] Rebase your commits based on master branch of dreal/dreal3 repository.