Nikolaj Bjorner
|
2097983db3
|
fix java bindings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-04 14:05:38 -07:00 |
|
Nikolaj Bjorner
|
b540868cd7
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-10-04 13:43:04 -07:00 |
|
Nikolaj Bjorner
|
a549e73b86
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-04 13:43:01 -07:00 |
|
Nikolaj Bjorner
|
f8e5d989bf
|
fix #1577
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-03 17:49:57 -07:00 |
|
Nikolaj Bjorner
|
3bc2213d54
|
fix #1577
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-03 17:43:42 -07:00 |
|
Nikolaj Bjorner
|
46cdefac4d
|
fix memory leak when cuber isn't run to completion. Found by Daniel Selsam
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-03 10:57:02 -07:00 |
|
Nikolaj Bjorner
|
fd9fd52271
|
fixing #1847
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-02 17:13:46 -07:00 |
|
Nikolaj Bjorner
|
8b981e545d
|
Merge pull request #1855 from mtrberzi/refactoring-arith
Z3str3: refactoring, arith_value
|
2018-10-02 14:10:36 -07:00 |
|
Nikolaj Bjorner
|
42fd3da5c5
|
Merge pull request #1854 from janisozaur/intel-compiler
Add support for Intel Compiler
|
2018-10-02 11:55:21 -07:00 |
|
Nikolaj Bjorner
|
69f35a2970
|
Merge branch 'master' into intel-compiler
|
2018-10-02 11:54:52 -07:00 |
|
Murphy Berzish
|
b2f0051114
|
Merge remote-tracking branch 'upstream/master' into refactoring-arith
|
2018-10-02 12:38:40 -04:00 |
|
Murphy Berzish
|
39fbf1e174
|
Z3str3: don't use arith_value::get_value in get_arith_value
|
2018-10-02 12:28:53 -04:00 |
|
Nikolaj Bjorner
|
55cc89b6bb
|
Merge pull request #1862 from kbobyrev/arith_eq_solver-cleanup
[NFC] Cleanup arith_eq_solver.(cpp|h)
|
2018-10-02 08:48:49 -07:00 |
|
Nikolaj Bjorner
|
cc312d2f68
|
Merge pull request #1861 from waywardmonkeys/macos-naming
Refer to macOS rather than Mac OS / OSX.
|
2018-10-02 08:28:02 -07:00 |
|
Nikolaj Bjorner
|
5bf57c2700
|
fix cubing semantics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-02 08:14:19 -07:00 |
|
Kirill Bobyrev
|
a376a8d343
|
[NFC] Cleanup arith_eq_solver.(cpp|h)
Use for-range loops instead of for-index loops where possible, remove
trailing whitespaces.
This patch does not affect functionality.
|
2018-10-02 16:14:01 +03:00 |
|
Bruce Mitchener
|
a76397d3b8
|
Refer to macOS rather than Mac OS / OSX.
|
2018-10-02 17:38:09 +07:00 |
|
Nikolaj Bjorner
|
620c5d1d81
|
Merge pull request #1850 from Nils-Becker/master
adding call to update_max_generation
|
2018-10-01 21:49:14 -07:00 |
|
Nikolaj Bjorner
|
2cf6ada38e
|
Merge pull request #1856 from waywardmonkeys/minor-fixes
Minor fixes
|
2018-10-01 20:46:27 -07:00 |
|
Nikolaj Bjorner
|
c84182b42a
|
Merge pull request #1859 from waywardmonkeys/for-range-copy
Avoid unnecessary copies in for-range loops.
|
2018-10-01 20:44:52 -07:00 |
|
Nikolaj Bjorner
|
7082d85115
|
Merge pull request #1860 from waywardmonkeys/modernize-use-override
Use 'override' where possible.
|
2018-10-01 20:43:56 -07:00 |
|
Bruce Mitchener
|
6d2936e5fc
|
watch_list: Fix indentation.
|
2018-10-02 10:43:00 +07:00 |
|
Bruce Mitchener
|
1067a5363f
|
theory_lra: Remove unused variable.
|
2018-10-02 10:42:54 +07:00 |
|
Bruce Mitchener
|
7bc283b84e
|
Avoid unnecessary copies in for-range loops.
|
2018-10-02 10:38:41 +07:00 |
|
Bruce Mitchener
|
373b691709
|
Use 'override' where possible.
|
2018-10-02 10:26:38 +07:00 |
|
Nikolaj Bjorner
|
5eb24d3118
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-10-01 20:22:10 -07:00 |
|
Nikolaj Bjorner
|
9d0aa4d02d
|
update empty cube case for sat/undef cases
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-01 20:22:02 -07:00 |
|
Nikolaj Bjorner
|
3c7e7a7ffd
|
Merge pull request #1852 from janisozaur/unused-const
Drop unused CV-qualifiers from scalar return values
|
2018-10-01 20:10:21 -07:00 |
|
Nikolaj Bjorner
|
4bc6720af7
|
Merge pull request #1853 from janisozaur/solve-ax-eq-b
Add missing template instantion for lar_core_solver::m_r_solver
|
2018-10-01 20:09:50 -07:00 |
|
Nikolaj Bjorner
|
be8a9c611e
|
incorporate #1854
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-01 19:49:18 -07:00 |
|
Nikolaj Bjorner
|
096a6c088d
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-10-01 19:32:52 -07:00 |
|
Nikolaj Bjorner
|
bb979a194e
|
remove unused return value of mk_enode following #1856
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-01 19:32:44 -07:00 |
|
Nikolaj Bjorner
|
b0dac346dc
|
Merge pull request #1857 from waywardmonkeys/modernize-use-nullptr
Use nullptr.
|
2018-10-01 19:28:58 -07:00 |
|
Nikolaj Bjorner
|
b2430f5a0a
|
Merge pull request #1858 from waywardmonkeys/remove-unused-sat-par
Remove unused sat_par files.
|
2018-10-01 19:26:46 -07:00 |
|
Bruce Mitchener
|
489582f7fa
|
Remove unused sat_par files.
These look like they were replaced by `sat_parallel` files and
aren't currently built or used.
|
2018-10-02 09:19:14 +07:00 |
|
Bruce Mitchener
|
cdfc19a885
|
Use nullptr.
|
2018-10-02 09:11:19 +07:00 |
|
Nikolaj Bjorner
|
808d2eb60f
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-10-01 15:52:25 -07:00 |
|
Nikolaj Bjorner
|
08c58ae614
|
make the unsat/sat verdicts from cubing produce empty clause and models respectively
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-01 15:52:22 -07:00 |
|
Murphy Berzish
|
03d9047490
|
Merge remote-tracking branch 'upstream/master' into refactoring-arith
|
2018-10-01 17:51:12 -04:00 |
|
Michał Janiszewski
|
5c9b1c7b11
|
Add support for Intel Compiler
|
2018-10-01 21:45:01 +02:00 |
|
Michał Janiszewski
|
661826e27f
|
Add missing template instantion for lar_core_solver::m_r_solver
|
2018-10-01 21:35:48 +02:00 |
|
Christoph M. Wintersteiger
|
aaae3118de
|
CI Test
|
2018-10-01 20:26:05 +01:00 |
|
Christoph M. Wintersteiger
|
f145873603
|
CI Test
|
2018-10-01 20:22:20 +01:00 |
|
Michał Janiszewski
|
cdbfd9654f
|
Drop unused CV-qualifiers from scalar return values
|
2018-10-01 21:14:25 +02:00 |
|
Christoph M. Wintersteiger
|
7a2a2a32cc
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2018-10-01 17:25:14 +01:00 |
|
Christoph M. Wintersteiger
|
48ec7c1175
|
Follow-up fix for fpa2bv_converter.
|
2018-10-01 17:25:02 +01:00 |
|
Nikolaj Bjorner
|
75b77979fe
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-10-01 09:18:46 -07:00 |
|
Nikolaj Bjorner
|
aaba1b9b15
|
fix sort retrieval for lambdas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-10-01 09:18:40 -07:00 |
|
nilsbecker
|
c92c431570
|
adding call to update_max_generation
|
2018-10-01 16:32:04 +02:00 |
|
Christoph M. Wintersteiger
|
2a92de0aee
|
Fixed side conditions for UFs translated from FP to BV. Fixes #1825.
|
2018-10-01 15:20:00 +01:00 |
|