Skip to content

Rollback to support yices again #1714

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
feliam merged 33 commits into from
Jun 9, 2020
Merged

Rollback to support yices again #1714

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
33 commits
Select commit Hold shift + click to select a range
165bb47
Rollback to support yices again
feliam May 21, 2020
c43036a
CC
feliam May 21, 2020
9cb8ae3
Test yices
feliam May 21, 2020
69337d0
Better get-value handling
feliam May 21, 2020
b4c899d
Z3/CVC4/YICES
feliam May 22, 2020
09b0374
CC
feliam May 23, 2020
0649f85
Yices/CVC4
feliam May 26, 2020
2af40be
CC
feliam May 26, 2020
57aa187
Default yices
feliam May 26, 2020
0cdbaed
Default debug level fix
feliam May 26, 2020
5c17309
Quick auto solver
feliam May 26, 2020
a92cb6e
shutil.which
feliam May 26, 2020
3d91266
CC
feliam May 26, 2020
60e020b
Default yices for testing
feliam May 27, 2020
afcd693
Remove old commented out code
feliam May 27, 2020
20f846d
Update manticore/core/smtlib/solver.py
feliam May 28, 2020
a60a6e7
Update manticore/core/smtlib/solver.py
feliam May 28, 2020
82f2f88
Merge branch 'dev-yikes' of github.com:trailofbits/manticore into dev…
feliam May 28, 2020
e4e3a65
Remove unused class
feliam May 28, 2020
af19863
Update manticore/core/smtlib/solver.py
feliam May 28, 2020
3061b7c
Update manticore/core/smtlib/solver.py
feliam May 28, 2020
38c888b
Readme hack
feliam May 28, 2020
9c27f1c
Merge branch 'dev-yikes' of github.com:trailofbits/manticore into dev…
feliam May 28, 2020
6db6e77
CC/lint
feliam May 28, 2020
3e68a85
Fix typing
feliam May 28, 2020
5a97426
z3 back to the rodeo
feliam May 29, 2020
3ddb5b6
lint
feliam Jun 2, 2020
744dfde
Merge branch 'master' into dev-yikes
feliam Jun 2, 2020
2391ca1
Fancy optimize
feliam Jun 2, 2020
07a8b40
Merge branch 'master' into dev-yikes
feliam Jun 4, 2020
05071bf
Fix lint
feliam Jun 5, 2020
8a3c6c0
Merge branch 'master' into dev-yikes
feliam Jun 9, 2020
3f11904
CC reviewed
feliam Jun 9, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,13 @@ jobs:
env:
TEST_TYPE: ${{ matrix.type }}
run: |
#install cvc4
sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
sudo chmod +x /usr/bin/cvc4
#install yices
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
Comment thread
feliam marked this conversation as resolved.
# Install solc unconditionally because it only takes a second or two
sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux
sudo chmod +x /usr/bin/solc
Expand Down
4 changes: 4 additions & 0 deletions manticore/core/smtlib/expression.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -770,6 +770,10 @@ def __getitem__(self, index):
raise IndexError
return self.select(self.cast_index(index))

def __iter__(self):
for i in range(len(self)):
yield self[i]

def __eq__(self, other):
# FIXME taint
def compare_buffers(a, b):
Expand Down
Loading