3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Commit graph

667 commits

Author SHA1 Message Date
Leonardo de Moura a430d53475 merged 2012-12-06 15:35:54 -08:00
Leonardo de Moura 26f616268e fixed warning in 32bit sys
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 15:35:28 -08:00
Leonardo de Moura 017176c720 fixed messy directory separator in mk_util
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 15:33:43 -08:00
Leonardo de Moura db6e20b2ea cleaning mk_make
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 14:57:07 -08:00
Leonardo de Moura fdb3e22560 fixed mk_make problem on Windows
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 13:57:35 -08:00
Leonardo de Moura 68b97024e2 added missing option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 08:54:00 -08:00
Leonardo de Moura 75739fdf7b fixed memory smash
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-06 08:19:42 -08:00
Leonardo de Moura 294d40889f Merge branch 'nikolaj' into unstable 2012-12-06 07:42:50 -08:00
Nikolaj Bjorner dbde71c290 fixing unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-06 07:38:53 -08:00
Nikolaj Bjorner 6bdde9047a fixing unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-06 07:38:50 -08:00
Leonardo de Moura 3cefa0a1f7 making tests deterministic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 19:20:48 -08:00
Josh Berdine 2f3daf14b5 Regenerate ml api 2012-12-05 19:20:48 -08:00
Josh Berdine 6fad07e6e1 Update build system for ml api 2012-12-05 19:20:47 -08:00
Josh Berdine 949317ccfc Fixes for error handling in ml api 2012-12-05 19:20:47 -08:00
Josh Berdine ae5f96895d Change to avoid relying on sed supporting disjunction or escaped control characters 2012-12-05 19:20:47 -08:00
Josh Berdine 4ec4151e82 Change treatment of unsigned to avoid depending on unspecified behavior of recursive macros 2012-12-05 19:20:47 -08:00
Leonardo de Moura 1a11196211 fixing bug introduced today
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 16:21:53 -08:00
Leonardo de Moura 2b66b50c75 making tests deterministic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 16:21:38 -08:00
Leonardo de Moura 5e4d1151eb fixing clang compilation problems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 15:20:16 -08:00
Leonardo de Moura 3736c5ea3b removed template specialization overkill
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 08:56:19 -08:00
Leonardo de Moura 5379130c8c eliminated m_proof_mode from smt_params, ast_manager has this information
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-05 08:35:03 -08:00
Leonardo de Moura f6a3ec58e5 allow --help, --version, etc as valid parameter names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 15:48:28 -08:00
Leonardo de Moura 89385b4e9a no need for / options 2012-12-04 15:38:16 -08:00
Leonardo de Moura 6f5f1b290e better error message for renamed parameter names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 15:33:21 -08:00
Leonardo de Moura 2eef4cc1e7 forgot synch
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 11:59:46 -08:00
Leonardo de Moura bce9d1440b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-04 11:57:00 -08:00
Leonardo de Moura 92a29b1e43 added Z3_global_param_reset_all API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 11:55:12 -08:00
Christoph M. Wintersteiger fda39bffe2 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-04 19:33:11 +00:00
Christoph M. Wintersteiger 334ec57ea4 Java API: refactoring
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-12-04 19:33:01 +00:00
Christoph M. Wintersteiger acd251e554 .NET API: bugfix.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-12-04 19:32:46 +00:00
Christoph M. Wintersteiger 4d1d784a1c Java+.Net Examples: refactoring
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-12-04 19:32:20 +00:00
Leonardo de Moura 7d24cd4ae3 merged
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 11:18:10 -08:00
Leonardo de Moura ff999773b2 adjusting verbose msgs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 11:17:24 -08:00
Leonardo de Moura 9754ccf8a1 fixing problems with the new parameter framework
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 11:16:42 -08:00
Josh Berdine f7528456da Fix slight inconsistencies in use of \sa 2012-12-04 03:44:00 +00:00
Leonardo de Moura 8191cc1951 fixed problems with logger and invalid assertion
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-03 18:44:27 -08:00
Leonardo de Moura f0f90eecaa Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-03 16:58:56 -08:00
Leonardo de Moura 54e452a1af chasing bug in the Java bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-03 16:58:44 -08:00
Nikolaj Bjorner 1cd1a42618 cleanup, fix repeated use of fmls in validator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-03 16:02:04 -08:00
Leonardo de Moura 0ec6e2f218 adjusting examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-03 15:19:47 -08:00
Nikolaj Bjorner 72e09759ee factor out relation context for datalog
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-03 15:13:45 -08:00
Nikolaj Bjorner 67183ea08a factor out relation context for datalog
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-03 15:05:43 -08:00
Leonardo de Moura 6d7d205e13 fixed more problems in the new param framework
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-03 15:02:34 -08:00
Leonardo de Moura d634c945bf renamed validate_model --> model_validate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-03 13:44:39 -08:00
Leonardo de Moura 847c5f9691 fixing problems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-03 11:55:24 -08:00
Nikolaj Bjorner 8425685ea3 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-03 11:02:08 -08:00
Nikolaj Bjorner 5c11f394cd port to new parameter infrastructure
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-03 11:01:33 -08:00
Christoph M. Wintersteiger 006822a931 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-03 17:57:38 +00:00
Christoph M. Wintersteiger eb3fa254d8 Java API: bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2012-12-03 17:56:42 +00:00
Leonardo de Moura 8744b26d06 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-03 09:37:57 -08:00