From a7e0f18482e69a2eb8c78e91f6f59f1c40310800 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Mar 2018 16:53:04 -0700 Subject: [PATCH 1/9] vsts cmd Signed-off-by: Nikolaj Bjorner --- vsts.cmd | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 vsts.cmd diff --git a/vsts.cmd b/vsts.cmd new file mode 100644 index 000000000..7dbd84cd1 --- /dev/null +++ b/vsts.cmd @@ -0,0 +1,5 @@ +md build +cd build +set +cmake -G "NMake Makefiles" ../ +nmake From b82214ef0de966bd919ef1d58ba461dfa50a1953 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Mar 2018 16:59:41 -0700 Subject: [PATCH 2/9] try paths to vsvars Signed-off-by: Nikolaj Bjorner --- vsts.cmd | 2 ++ 1 file changed, 2 insertions(+) diff --git a/vsts.cmd b/vsts.cmd index 7dbd84cd1..8d715f6a0 100644 --- a/vsts.cmd +++ b/vsts.cmd @@ -1,5 +1,7 @@ md build cd build set +"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" +%VS140COMNTOOLS%\vcvars64.bat cmake -G "NMake Makefiles" ../ nmake From 785b7f3e6a3f3e2a05421d68cc2b75f6a88004d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Mar 2018 17:03:06 -0700 Subject: [PATCH 3/9] vsts cmd Signed-off-by: Nikolaj Bjorner --- vsts.cmd | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/vsts.cmd b/vsts.cmd index 8d715f6a0..8ef516423 100644 --- a/vsts.cmd +++ b/vsts.cmd @@ -1,7 +1,6 @@ md build cd build set -"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" -%VS140COMNTOOLS%\vcvars64.bat +call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" cmake -G "NMake Makefiles" ../ nmake From afb12fe6c352867da96d3993ef12df1fec27e599 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Mar 2018 17:22:58 -0700 Subject: [PATCH 4/9] move script Signed-off-by: Nikolaj Bjorner --- vsts.cmd => scripts/vsts.cmd | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename vsts.cmd => scripts/vsts.cmd (100%) diff --git a/vsts.cmd b/scripts/vsts.cmd similarity index 100% rename from vsts.cmd rename to scripts/vsts.cmd From 8602c52bc93045133880ee547cba344223949665 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Mar 2018 10:41:42 -0700 Subject: [PATCH 5/9] fix test build Signed-off-by: Nikolaj Bjorner --- scripts/vsts.cmd | 3 +++ src/test/sat_local_search.cpp | 6 +----- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/scripts/vsts.cmd b/scripts/vsts.cmd index 8ef516423..6f15e1bc3 100644 --- a/scripts/vsts.cmd +++ b/scripts/vsts.cmd @@ -4,3 +4,6 @@ set call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" cmake -G "NMake Makefiles" ../ nmake +nmake test-z3 +git pull https://github.com/z3prover/z3test z3test +cd z3test diff --git a/src/test/sat_local_search.cpp b/src/test/sat_local_search.cpp index fc1445e34..c9e3a18ec 100644 --- a/src/test/sat_local_search.cpp +++ b/src/test/sat_local_search.cpp @@ -92,16 +92,12 @@ void tst_sat_local_search(char ** argv, int argc, int& i) { switch (argv[i + 1][1]) { case 's': // seed v = atoi(argv[i + 2]); - local_search.config().set_seed(v); + local_search.config().set_random_seed(v); break; case 't': // cutoff_time v = atoi(argv[i + 2]); cutoff_time = v; break; - case 'i': // strategy_id - v = atoi(argv[i + 2]); - local_search.config().set_strategy_id(v); - break; case 'b': // best_known_value v = atoi(argv[i + 2]); local_search.config().set_best_known_value(v); From a873cc41bfa56109a8280fcbcec30342f57a4567 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Mar 2018 10:43:59 -0700 Subject: [PATCH 6/9] update vsts script Signed-off-by: Nikolaj Bjorner --- scripts/vsts.cmd | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/scripts/vsts.cmd b/scripts/vsts.cmd index 6f15e1bc3..09480038a 100644 --- a/scripts/vsts.cmd +++ b/scripts/vsts.cmd @@ -1,9 +1,15 @@ +rem Build md build cd build -set call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat" cmake -G "NMake Makefiles" ../ nmake + +rem Run unit tests nmake test-z3 +test-z3.exe -a + +cd .. +rem Run regression tests git pull https://github.com/z3prover/z3test z3test cd z3test From 7a64c82d994ec9788745d297a3893df481dc0916 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Mar 2018 11:15:49 -0700 Subject: [PATCH 7/9] comment out pull Signed-off-by: Nikolaj Bjorner --- scripts/vsts.cmd | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/vsts.cmd b/scripts/vsts.cmd index 09480038a..4f0b3a9b5 100644 --- a/scripts/vsts.cmd +++ b/scripts/vsts.cmd @@ -11,5 +11,5 @@ test-z3.exe -a cd .. rem Run regression tests -git pull https://github.com/z3prover/z3test z3test -cd z3test +rem git pull https://github.com/z3prover/z3test z3test +rem cd z3test From 7ded2a90e6271758804422f417138fb42292d993 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Mar 2018 11:55:18 -0700 Subject: [PATCH 8/9] remove unreachable from vector Signed-off-by: Nikolaj Bjorner --- scripts/vsts.cmd | 15 +++++++++++++-- src/util/vector.h | 1 - 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/scripts/vsts.cmd b/scripts/vsts.cmd index 4f0b3a9b5..0257fd929 100644 --- a/scripts/vsts.cmd +++ b/scripts/vsts.cmd @@ -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 diff --git a/src/util/vector.h b/src/util/vector.h index d2beacfb4..bdde50f83 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -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(m_data) - 2; From ba2e28fa0e9766b02a4840888ee1d57298c45ce2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Mar 2018 14:55:38 -0700 Subject: [PATCH 9/9] update build script Signed-off-by: Nikolaj Bjorner --- scripts/vsts.cmd | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/vsts.cmd b/scripts/vsts.cmd index 0257fd929..639e2f82d 100644 --- a/scripts/vsts.cmd +++ b/scripts/vsts.cmd @@ -17,7 +17,7 @@ rem Build and run examples rem Build and run unit tests nmake test-z3 -test-z3.exe -a +rem test-z3.exe -a cd ..