3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Commit graph

7955 commits

Author SHA1 Message Date
Pierre Pronchery 5f7bd993de Add support for NetBSD
Originally from David Holland <dholland@NetBSD.org>.
2018-03-13 21:59:35 +01:00
Nikolaj Bjorner 5651d00751 fix #1534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-12 13:21:31 -07:00
Nikolaj Bjorner 3d9139f6ef bump revision
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 12:07:55 -08:00
Nikolaj Bjorner 5854492504 add stdbool.h to see whether build system breaks #1526
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 11:59:42 -08:00
Nikolaj Bjorner fb3498cd0b
Merge pull request #1528 from DeforaNetworks/khorben/configure-parameters
Fix parameter expansion when configuring Z3
2018-03-10 14:42:01 -05:00
Nikolaj Bjorner 0ce2001449 fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 11:39:22 -08:00
Nikolaj Bjorner 6e87622c8a remove references to deprecated uses of PROOF_MODE #1531
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 13:55:01 -05:00
Nikolaj Bjorner e5a1981694 disable GCC flag change to see if this affects build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-09 15:40:35 -05:00
Pierre Pronchery ae165a539e Fix parameter expansion when configuring Z3 2018-03-09 14:20:31 +01:00
Nikolaj Bjorner db63c9299c Merge branch 'master' of https://github.com/z3prover/z3 2018-03-09 05:32:15 -05:00
Nikolaj Bjorner ba603307fc remove stale deprecated annotation #1525
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-09 05:32:01 -05:00
Nikolaj Bjorner fc835ba01e
Merge pull request #1518 from waywardmonkeys/const-proof-checker
Make proof_checker more const correct.
2018-03-09 05:22:49 -05:00
Nikolaj Bjorner 4e31794c44
Merge pull request #1519 from waywardmonkeys/colorize-output-with-ninja
Force color output with Ninja.
2018-03-09 05:18:50 -05:00
Nikolaj Bjorner 895d30a1ff
Merge pull request #1527 from waywardmonkeys/fix-typos
Fix typos.
2018-03-09 05:18:01 -05:00
Bruce Mitchener 878a6ca14f Fix typos. 2018-03-09 14:30:43 +07:00
Nikolaj Bjorner 4f9d198c51
Merge pull request #1517 from mtrberzi/issue1379
Handle third argument of str.indexof in Z3str3
2018-03-08 14:19:01 -08:00
Murphy Berzish bf6975122b integrate contains and indexof in theory_str 2018-03-08 12:37:44 -05:00
Nikolaj Bjorner 02a9696701 fix #1521
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-08 11:19:00 -05:00
Murphy Berzish d1407e843d Merge branch 'issue1379' of github.com:mtrberzi/z3 into issue1379 2018-03-07 18:16:17 -05:00
Murphy Berzish a7caa2fd2a remove useless get_assignments in theory_str final check 2018-03-07 18:16:11 -05:00
Nikolaj Bjorner 246941f2d3 fix #1522
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-07 14:26:38 -08:00
Murphy Berzish fd6d9a9489 Merge branch 'issue1379' of github.com:/mtrberzi/z3 into issue1379 2018-03-07 13:54:45 -05:00
Bruce Mitchener 0b54a91513 Force color output with Ninja. 2018-03-07 13:29:13 +07:00
Bruce Mitchener 4cc9362851 Make proof_checker more const correct. 2018-03-07 13:18:39 +07:00
Murphy Berzish f43a027447 Merge branch 'develop' into issue1379 2018-03-06 22:14:18 -05:00
Nikolaj Bjorner eb1122c5cb delay updating parameters to ensure rewriting in asserted_formulas is applied using configuration overrides. Fixes build regression for tree_interpolation documentation test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-04 21:57:08 -08:00
Nikolaj Bjorner 534a31f74e inherit solver parameters in asserted formulas rewriter. #1511
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-04 05:06:36 -08:00
Nikolaj Bjorner a64fd7145c remove buggy legacy code, rely on pull_cheap_ite option in rewriter, #1511
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-04 03:36:03 -08:00
Nikolaj Bjorner 205d77d591 save last model to ensure it is available fixes #1514
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-03 19:26:31 -08:00
Nikolaj Bjorner 8e09a78c26 fix #1510 by reintroducing automatic declaration of recognizers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-02 23:02:20 +09:00
Nikolaj Bjorner a738f5af12 fix #1512
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-02 20:14:59 +09:00
Nikolaj Bjorner 00c3f4fdcd fix bugs found while running sample from #1112 in debug mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-28 22:35:41 +09:00
Nikolaj Bjorner 30de514a88 fix topological traversal crash
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-28 11:59:17 +09:00
Nikolaj Bjorner b79d1a6956 fix #1488 for smtlib basic printer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-28 09:22:20 +09:00
Nikolaj Bjorner fbbc57168d
Merge pull request #1508 from mtrberzi/regex-allchar
add re.allchar support in z3str3
2018-02-27 09:12:13 +09:00
Murphy Berzish ac9b03528a add re.allchar support in z3str3 2018-02-26 17:19:45 -05:00
Nikolaj Bjorner 5d457c95aa update registration of built-ins
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-26 21:00:41 +09:00
Nikolaj Bjorner 0199c7515f fix z3.py
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-26 19:49:13 +09:00
Nikolaj Bjorner ce1b135ec3 address accessor inconsistencies between - and from #1506
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-26 14:57:17 +09:00
Nikolaj Bjorner 45b6e0998a Merge branch 'master' of https://github.com/z3prover/z3 2018-02-25 13:19:59 +09:00
Nikolaj Bjorner e9b6de0746
Merge pull request #1501 from mikhailramalho/master
Convert BVULT(X,Y) into !BVULE(Y,X)
2018-02-25 13:19:11 +09:00
Nikolaj Bjorner d5f83205ac
Merge pull request #1495 from AngusL/master
Fix Python FiniteDomainSortRef.size()
2018-02-25 13:16:17 +09:00
Nikolaj Bjorner 5741786f3e
Merge pull request #1503 from cocreature/fid-order
Fix assignment of family ids
2018-02-25 13:15:40 +09:00
Nikolaj Bjorner 314c39de99
Merge pull request #1497 from levnach/dev
fix the override warning
2018-02-25 13:13:33 +09:00
Nikolaj Bjorner 7b68be75c9 fixes to #1500 and #1457
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-25 13:11:20 +09:00
Nikolaj Bjorner 9279cbfbac don't reinit assumptions when the solver is unsat. fixes #1502
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-24 16:30:08 +09:00
Moritz Kiefer 5d0e33c9ad Fix assignment of family ids 2018-02-23 20:22:07 +01:00
Mikhail Ramalho c5336f8003 Convert BVULT(X,Y) into !BVULE(Y,X)
Signed-off-by: Mikhail Ramalho <mikhail.ramalho@gmail.com>
2018-02-23 17:17:02 +00:00
Lev Nachmanson a238a0a37d fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2018-02-22 17:07:21 -08:00
Lev Nachmanson dbe5df85c3 fix the override warning
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2018-02-22 08:44:50 -08:00