mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 09:49:23 +00:00
Code Activity
7955 commits 45 branches 52 tags 177 MiB
Commit graph

7955 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
712619a9cf fix a but in adjusting term indices for implied_bounds 2017-08-03 10:09:00 -07:00
Nikolaj Bjorner
ffaaa1ff34 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-03 08:50:17 -07:00
Nikolaj Bjorner
8844112418 update header include generation to use relative paths #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 08:50:04 -07:00
Nikolaj Bjorner
06e48c89f2 Merge branch 'master' of https://github.com/z3prover/z3 2017-08-02 16:56:51 -07:00
Nikolaj Bjorner
4b3251dec1 update API functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-02 16:56:43 -07:00
Nikolaj Bjorner
d12a0133ce Merge pull request #1189 from delcypher/travis_ci_wait_longer_when_no_output 
[TravisCI] Try to make the LTO build more reliable.
 2017-08-02 08:47:09 -07:00
Dan Liew
c2f69ae9fb [TravisCI] Try to make the LTO build more reliable. 
TravisCI kills builds that don't show output for over 10 minutes [1].
This sometimes causes LTO builds to fail because gcc shows no output
during linking which can take many minutes to complete.

To workaround this we use the `travis_wait` command to allow at
most 45 minutes for the build to run. This command will force output
to appear at regular intervals.

The change is made in the top-level `.travis.yml` file rather than
the other scripts because I don't want to pollute them with TravisCI
specific details.

[1] https://docs.travis-ci.com/user/common-build-problems/#Build-times-out-because-no-output-was-received
 2017-08-02 11:58:47 +01:00
Nikolaj Bjorner
ce3fd22f3b use common idioms for factor-equivalence code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 21:07:20 -07:00
Nikolaj Bjorner
0a6759383a Merge pull request #1188 from agurfinkel/move_obj_equiv 
moved obj_equiv_class to ast
 2017-08-01 20:05:37 -07:00
Arie Gurfinkel
88a35119b9 moved obj_equiv_class to ast 2017-08-01 19:24:50 -04:00
Nikolaj Bjorner
4d07fa5db3 use ifdef instead of if for _TRACE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 12:46:38 -07:00
Nikolaj Bjorner
be8add44e9 instrument unit test to use reproducible random number generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 12:42:08 -07:00
Nikolaj Bjorner
22a2aae486 trying to fix build break on use of iterator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 11:47:55 -07:00
Nikolaj Bjorner
3214644e0d Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-01 10:51:52 -07:00
Nikolaj Bjorner
2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Christoph M. Wintersteiger
49d5131f83 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-01 18:33:59 +01:00
Christoph M. Wintersteiger
81a7f37acc Fixed LP tests 2017-08-01 18:33:47 +01:00
Christoph M. Wintersteiger
13c9a6faf7 Merge pull request #1185 from agurfinkel/spacer-nlg-fix 
Spacer nlg fix
 2017-08-01 17:23:23 +01:00
Christoph M. Wintersteiger
aefed78f1a Fixed ML API build again 2017-08-01 17:02:04 +01:00
Christoph M. Wintersteiger
ce01895ab3 Fixed ML API build. 2017-08-01 16:54:27 +01:00
Christoph M. Wintersteiger
4ff938f2c1 Fixed MPF fp.rem(0,0,0). Relates to #872. 2017-08-01 16:46:10 +01:00
Bernhard Gleiss
4559092a0c refactored variable names and added comments to min_cut-related methods for unsat-core-computation 2017-08-01 11:17:06 -04:00
Bernhard Gleiss
bc3d8580c9 fixed typo in optimized unsat core plugin code 2017-08-01 11:17:06 -04:00
Christoph M. Wintersteiger
79ab8a5a5a Fixed cmake build 2017-08-01 16:16:17 +01:00
Christoph M. Wintersteiger
e315d063c5 renamed LP bound propagator to avoid linker name clashes 2017-08-01 16:07:51 +01:00
Christoph M. Wintersteiger
6bc5209e26 Fixed build problems with .vcxproj 2017-08-01 15:53:55 +01:00
Nikolaj Bjorner
72c478078e adding cdecl directive to Z3_qe_lite to address build failure for Java bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 23:14:53 -07:00
Nikolaj Bjorner
1820ccd491 z3-qe-lite? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 22:15:57 -07:00
Nikolaj Bjorner
b12882d94a a few more spacer related warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 21:56:13 -07:00
Nikolaj Bjorner
9a78bec8a8 Merge pull request #1183 from agurfinkel/spacer-z3 
removing pragmas to make travis happy
 2017-07-31 21:44:00 -07:00
Arie Gurfinkel
25c6480e6e updated include directives 2017-07-31 23:16:42 -04:00
Arie Gurfinkel
ecd85b314c more includes 2017-07-31 22:51:28 -04:00
Arie Gurfinkel
66108085fa removing pragmas to make travis happy 2017-07-31 22:51:28 -04:00
Nikolaj Bjorner
c506f3ddc9 fix build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 18:39:35 -07:00
Nikolaj Bjorner
0eb2915e83 Merge pull request #1182 from agurfinkel/spacer-z3 
Spacer
 2017-07-31 17:10:09 -07:00
Nikolaj Bjorner
49cf899207 remove local change 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 16:33:48 -07:00
Nikolaj Bjorner
5cda9504f1 remove relative include from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 16:32:26 -07:00
Christoph M. Wintersteiger
e8cdc34219 Debug fix in fpa2bv converter. Relates to #872. 2017-07-31 22:34:58 +01:00
Arie Gurfinkel
ffff16632d updating includes 2017-07-31 17:30:11 -04:00
Arie Gurfinkel
f465a2225a fixing include paths 2017-07-31 17:14:43 -04:00
Christoph M. Wintersteiger
6a2fa91818 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 22:12:37 +01:00
Christoph M. Wintersteiger
9601761a6f Added missing float conversion in fpa2bv converter. Relates to #1178. 2017-07-31 22:12:15 +01:00
Nikolaj Bjorner
8fdf3177da add initialization to unused parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 14:06:29 -07:00
Arie Gurfinkel
97c5ab30d5 small improvements to bmc engine 
courtesy of Marc Brockschmidt
 2017-07-31 17:04:36 -04:00
Arie Gurfinkel
7168451201 eager quantifier instantiation for quantified array properties 2017-07-31 17:04:16 -04:00
Arie Gurfinkel
2c7a39d580 Optionally blast arrays 
This changes the default behavior of always blasting arrays.
The old behavior can be restored using

   fixedpoint.xform.array_blast=true
 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
f5fa6b0bcb optionally disable subsumption checker 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
33c81524d2 optionally disable propagate variable equivalences in interp_tail_simplifier 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
86db446afa python spacer-specific API 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
d080c146a2 public API for spacer 2017-07-31 17:03:18 -04:00