Daniel Perelman
b06b9eeb35
Adding ENABLE_CFI flag to CMake.
2017-07-26 16:31:28 -07:00
Christoph M. Wintersteiger
fd3727ad00
Merge pull request #1162 from delcypher/travis_ci_fix_running_unit_tests
...
[TravisCI] Fix running unit tests.
2017-07-26 11:20:03 +01:00
Dan Liew
cbca609af4
[TravisCI] Fix running unit tests.
...
Previously the `test-z3` executable was run without arguments which
appears to run no tests. To fix this the `/a` argument is passed
which will run all tests that don't require arguments.
This was noticed in #1159 when @KarenHuang2016 reported a failing
test.
2017-07-26 08:57:46 +01:00
Nikolaj Bjorner
9f9c575451
fix bug exposed when running test-z3.exe /a in debug mode, #1159 . Add assertions to heap interaction
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-25 16:26:45 -07:00
Nikolaj Bjorner
9d6be286d0
Merge branch 'master' of https://github.com/Z3Prover/z3
2017-07-25 10:18:43 -07:00
Nikolaj Bjorner
70f6280bf1
fix regression reported in #1159
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-25 10:18:21 -07:00
Nikolaj Bjorner
3865c45382
Merge pull request #1147 from mtrberzi/fix-get-arith-value
...
Improved theory_arith integration in theory_str::get_arith_value()
2017-07-24 21:21:45 -07:00
Nikolaj Bjorner
741f940119
Merge pull request #1158 from facanferff/master
...
pretty printer: fix typo with ReSort sort name
2017-07-24 21:19:18 -07:00
Nikolaj Bjorner
49f88d9d90
fix uninitialized warning
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-24 12:52:10 -07:00
Nikolaj Bjorner
a94f5fb04a
fix compiler warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-24 12:15:10 -07:00
Nikolaj Bjorner
ae5e39a8b8
Merge branch 'master' of https://github.com/z3prover/z3
2017-07-24 09:18:27 -07:00
Nikolaj Bjorner
7fd0777cf1
fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-24 09:18:16 -07:00
Nikolaj Bjorner
a0a8bc2a62
fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-24 09:12:43 -07:00
Fábio Ferreira
2e2782577b
pretty printer: fix typo with ReSort sort name
2017-07-23 02:32:35 +01:00
Christoph M. Wintersteiger
0f1583309d
Bugfix for fp.fma. One piece of puzzle #872 .
2017-07-21 21:12:45 +01:00
Christoph M. Wintersteiger
faa19117e4
Fixed inconsistent state upon solver interruption. Partially fixes #951 .
2017-07-21 17:42:48 +01:00
Christoph M. Wintersteiger
943dc8118a
Improved collect-statistics tactic
2017-07-20 13:44:47 +01:00
Murphy Berzish
7ddb940f77
add e_internalized() check in theory_str::get_arith_value()
2017-07-19 10:15:38 -04:00
Murphy Berzish
69f0ed9b1f
remove disabled code block in get_arith_value()
2017-07-18 13:13:12 -04:00
Murphy Berzish
c6707688ba
improved get_arith_value() in theory_str
...
Since the root of the eqc of an integer term should be a constant
if there is a constant in that eqc, we can ask for it directly
without either iterating over the entire eqc or
asking the arithmetic solver (and receiving potentially stale info).
2017-07-18 13:11:03 -04:00
Christoph M. Wintersteiger
da34de340d
Fixed bug in sat model converter. Fixes #1148 .
2017-07-15 20:25:13 +01:00
Nikolaj Bjorner
8a57e081f7
Merge pull request #1138 from delcypher/cmake_serious_warnings
...
Support serious warnings in CMake and TravisCI
2017-07-14 11:14:35 +02:00
Christoph M. Wintersteiger
680f342247
Merge pull request #1145 from delcypher/fix_doc_typo
...
Fix minor typo in C API documentation
2017-07-12 15:47:44 +01:00
Christoph M. Wintersteiger
baedf41c6c
Merge pull request #1144 from delcypher/fix_parse_bvsmod_i
...
Fix typo that prevented uses of `bvsmod_i` being parsed.
2017-07-12 15:47:24 +01:00
Dan Liew
5b511f12b3
Fix minor typo in C API documentation
2017-07-12 13:07:19 +01:00
Dan Liew
89c8f1722f
Fix typo that prevented uses of bvsmod_i
being parsed.
2017-07-12 12:53:10 +01:00
Christoph M. Wintersteiger
bf83b897a1
Merge pull request #1142 from jfeser/master
...
Add get_num_scopes to python solver api.
2017-07-11 21:29:50 +01:00
Jack Feser
0e45777104
add get_num_scopes to python solver api
2017-07-11 14:42:34 -04:00
Murphy Berzish
86e7f83e06
proper theory_arith integration in theory_str::get_arith_value()
2017-07-11 13:24:48 -04:00
Dan Liew
630863619b
[TravisCI] Add Z3_WARNINGS_AS_ERRORS
environment variable to
...
control the `WARNINGS_AS_ERRORS` CMake option.
2017-07-09 14:44:20 +01:00
Dan Liew
6e2ca69654
[CMake] Change the WARNINGS_AS_ERRORS
option from BOOL to STRING
...
to allow a new mode `SERIOUS_ONLY`.
Modes:
`ON` - All warnings are treated as errors (same as before)
`OFF` - Warnings are not treated as errors (same as before)
`SERIOUS_ONLY` - A subset of "serious" warnings are treated as errors.
Upgrade code is included to upgrade old CMake cache's to use the new
type of `WARNINGS_AS_ERRORS`. We should remove it eventually. The
user's previous setting is preserved when doing this.
Very few warnings are treated as errors for now. Developers can
add more later as they see fit.
2017-07-09 14:34:30 +01:00
Nikolaj Bjorner
2b0106c199
doc fixes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-09 11:26:27 +02:00
Nikolaj Bjorner
2af08a378d
avoid complaining about division by 0 as unhandled in theory-lra
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-08 18:21:47 -07:00
Nikolaj Bjorner
5714f830b0
fix check for finite sorts #1122
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-08 13:37:24 -07:00
Nikolaj Bjorner
ea331ebfbe
revert update to #1134
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-07 08:29:16 -07:00
Nikolaj Bjorner
d06e48a361
detect overlapping signatures #1134
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-07 08:13:14 -07:00
Nikolaj Bjorner
98391883ca
Merge branch 'master' of https://github.com/z3prover/z3
2017-07-07 07:45:00 -07:00
Nikolaj Bjorner
49cf3f8008
update documentation according to #1058
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-07 07:44:55 -07:00
Christoph M. Wintersteiger
4b895abec7
Merge pull request #1136 from danpere/guard-cf
...
Add flag to mk_make.py to optionally enable Control Flow Guard
2017-07-07 11:48:52 +01:00
Daniel Perelman
d57494395c
Add --guardcf flag to mk_make.py to optionally enable Control Flow Guard.
2017-07-06 16:59:20 -07:00
Nikolaj Bjorner
465ed7d068
adding doc #1132
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-05 10:21:57 -07:00
Nikolaj Bjorner
5357864dbe
Merge pull request #1131 from mtrberzi/fix-warnings-2
...
fix theory_str warnings: rename get_value() to get_arith_value()
2017-07-05 10:03:41 -07:00
Murphy Berzish
b14364a117
fix theory_str warnings: rename get_value() to get_arith_value()
2017-07-05 11:06:40 -04:00
Nikolaj Bjorner
41803ec1cf
fix trace/debug build for unreferenced variables
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 19:55:38 -07:00
Nikolaj Bjorner
cba9a160d3
deal with warning messages
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 19:42:22 -07:00
Nikolaj Bjorner
5b8e3ae198
Merge pull request #1129 from mtrberzi/fix-warnings
...
clean up warnings in theory_str
2017-07-04 19:41:43 -07:00
Nikolaj Bjorner
bd92797663
fix compiler warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 15:25:59 -07:00
Nikolaj Bjorner
d66db280a8
fix compiler warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 13:43:32 -07:00
Nikolaj Bjorner
a1306eaab6
fix compiler warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 13:17:37 -07:00
Nikolaj Bjorner
253870c6d7
fix compiler warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 13:08:23 -07:00