mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

remove unreachable from vector

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-19 11:55:18 -07:00
parent 7a64c82d99
commit 7ded2a90e6
2 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

15
scripts/vsts.cmd
View file

@ -2,13 +2,24 @@ rem Build
md build
cd build
call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"
cmake -G "NMake Makefiles" ../
cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "NMake Makefiles" ../
nmake
rem Run unit tests
rem test python bindings
pushd python
python z3test.py z3
python z3test.py z3num
popd
rem Build and run examples
rem Build and run unit tests
nmake test-z3
test-z3.exe -a
cd ..
rem Run regression tests
rem git pull https://github.com/z3prover/z3test z3test

1
src/util/vector.h
View file

@ -73,7 +73,6 @@ class vector {
SZ new_capacity = (3 * old_capacity + 1) >> 1;
SZ new_capacity_T = sizeof(T) * new_capacity + sizeof(SZ) * 2;
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
UNREACHABLE();
throw default_exception("Overflow encountered when expanding vector");
}
SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;