mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 02:41:52 +00:00
Code Activity
9833 commits 23 branches 48 tags 156 MiB
Commit graph

9833 commits

This branch
This branch
All branches
Author SHA1 Message Date
Andrew Helwer 8e0eb2ac50 Added NuGet package icon 2018-10-06 16:04:33 -07:00
Nikolaj Bjorner aad09816cb build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 15:16:23 -07:00
Nikolaj Bjorner c4829dfa22 fix #1577 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 09:01:01 -07:00
Nikolaj Bjorner 44a0dbbc61 fix #1864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 08:06:51 -07:00
Lev 99339798ee fix the value oflar_solver.m_status during pop() 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-10-04 19:43:01 -07:00
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