3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 10:51:50 +00:00
Commit graph

11231 commits

Author SHA1 Message Date
Everett Maus 73083977e2 Trying a different clang version that should be installed 2019-08-12 17:31:57 -07:00
Everett Maus 8e3f5b0c1d Add MSAN_SYMBOLIZER_PATH to the environment to get symbolization 2019-08-12 15:56:50 -07:00
Everett Maus ec36e232e5 Fixing a spacing issue when undoing a comment 2019-08-09 10:34:42 -07:00
Everett Maus 42b557cf90 Restoring commented out template 2019-08-09 10:33:47 -07:00
Everett Maus f1a713a116 Restoring commented out pipelines 2019-08-09 09:17:17 -07:00
Everett Maus d01aa01ec9 And some includes now. 2019-08-08 21:00:39 -07:00
Everett Maus 1ff11b36bd More syntax errors... 2019-08-08 20:54:29 -07:00
Everett Maus 0d89c02486 Missed a paren as well. 2019-08-08 20:53:47 -07:00
Everett Maus 85601453cd Missed a colon. 2019-08-08 20:52:25 -07:00
Everett Maus 179242ed29 More template changes... 2019-08-08 20:50:19 -07:00
Everett Maus 2bcd3280fa Testing a new configuration 2019-08-08 20:40:54 -07:00
Everett Maus 45c17dc256 Examples are still failing. 2019-08-08 20:01:38 -07:00
Everett Maus cc6f185e40 Examples are failing to build for strange reasons. 2019-08-08 19:59:20 -07:00
Everett Maus bf3bc1432f Fixing a bug. 2019-08-08 19:17:40 -07:00
Everett Maus 3dc898384f Fixing a chmod issue. 2019-08-08 19:12:05 -07:00
Everett Maus b96f0e4b7b Commenting out non-MSAN builds for testing 2019-08-08 19:08:06 -07:00
Everett Maus ed29e1ffa5 Second pass at getting MSAN working with azure pipelines 2019-08-08 18:36:33 -07:00
Everett Maus 9cccfb97ac Take one on adding MSAN 2019-08-08 09:16:54 -07:00
Nikolaj Bjorner e950453685 force propagation for smt cubing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-06 14:19:16 -07:00
Nikolaj Bjorner bbfac99b22 fix #2469
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-06 13:52:42 -07:00
Nikolaj Bjorner 0af249d651 'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-06 13:44:12 -07:00
Bruce Mitchener f90439fdc5 docs: Fix a number of identifier formatting issues. 2019-08-04 18:48:30 -07:00
Bruce Mitchener 077f518241 Fix -Wreorder warning. 2019-08-04 18:37:31 -07:00
Bruce Mitchener ce7f9c3f3d Remove unused variable. 2019-08-04 18:37:05 -07:00
Nikolaj Bjorner d977c151f6
Merge pull request #2462 from waywardmonkeys/fix-typo
Fix typo.
2019-08-04 18:00:55 -07:00
Bruce Mitchener 6be36f18c6 Fix typo. 2019-08-05 07:31:55 +07:00
Nikolaj Bjorner bc3b0f6e33 introduce fresh term when none is available in context or model to fix #2456
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-04 12:00:48 -07:00
Nikolaj Bjorner 01920abf46 introduce fresh term when none is available in context or model to fix #2456
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-04 11:57:30 -07:00
Nikolaj Bjorner 59f69bbe0d introduce fresh term when none is available in context or model to fix #2456
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-04 11:56:03 -07:00
Nikolaj Bjorner c7dc420b3b let me guess, ASAN doesn't like 0-byte memcpy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-03 23:19:59 -07:00
Nikolaj Bjorner 90415a18d3 fix build of test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-03 08:42:16 -07:00
Nikolaj Bjorner d7ac8dbc7d fix #2458
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-03 08:36:25 -07:00
Nikolaj Bjorner 3147d2351d fix #2460
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-03 08:06:38 -07:00
Nikolaj Bjorner 4431a534b3 fix #2450 - track assumptions across lazy explanations and variable equalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-03 07:57:16 -07:00
Nikolaj Bjorner db5af3088b logging for #2450
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-02 16:47:18 -07:00
Nikolaj Bjorner 1d488d07fa nlsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-02 15:06:34 -07:00
Nikolaj Bjorner 2d5714a5d4 fixing #2443 #2445 #2447 #2448
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-02 15:06:34 -07:00
Nikolaj Bjorner 584eee2cf4 fixing #2448 and #2445 and #2443
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-02 15:06:34 -07:00
Nikolaj Bjorner c4480337c4 fixing #2448 and #2445 and #2443
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-02 15:06:34 -07:00
Nikolaj Bjorner 3d1c40ce23 fixing #2448
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-02 15:06:34 -07:00
Lev Nachmanson 95eb0a0521 remove an unnecessary call m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j)
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2019-08-02 09:53:32 -07:00
Nikolaj Bjorner 294dcf7b1c
Merge pull request #2455 from levnach/fix
fix a bug in lar_solver in querying if a column is int
2019-08-02 08:19:34 +08:00
Lev Nachmanson e9e950062a fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2019-08-01 14:09:26 -07:00
Lev Nachmanson db5ac5afa8 fix a bug in lar_solver in queryaing if a column is int
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2019-08-01 11:51:56 -07:00
Nikolaj Bjorner 9d6728aa71 fix unsound rewrite
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-02 01:14:31 +08:00
Nikolaj Bjorner 0a29002c2f return unknown if m_array_weak was used and result is satisfiable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-02 00:20:41 +08:00
Nikolaj Bjorner 3f032e85e0 remove include of thread
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-01 16:34:37 +08:00
Nikolaj Bjorner bec38f268b remove debug code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-01 16:32:08 +08:00
Nikolaj Bjorner 7f073a0585 fix #2452 fix #2451
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-08-01 16:28:15 +08:00
Nikolaj Bjorner b7a27ca4bd
Merge pull request #2454 from RichardBradley/java_sudoku_example_fix
Fix sudoku Java example
2019-08-01 13:02:54 +08:00