3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Commit graph

24 commits

Author SHA1 Message Date
Dan Liew
a9fcfc531b [TravisCI][CMake] Add Z3_C_EXAMPLES_FORCE_CXX_LINKER CMake option
and propagate its value into the C API examples.

This flag forces the C API examples to use the C++ compiler as the
linker rather than the C compiler. This a workaround to avoid linking
errors when building with UBSan.
2017-10-16 08:56:17 +01:00
Nikolaj Bjorner
09ea370ea3 update C-example that fails to not use longjumps. Issue #1297
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-10 12:06:19 -07:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Takeshi Abe
5c2969c0f0 Fix typo 2016-03-23 12:51:41 +09:00
Christoph M. Wintersteiger
3b92128ed8 Fixed old-style C variable declaration problem in interpolation C example. 2016-02-16 12:12:59 +00:00
Ken McMillan
8b90bc9e91 fixed logginf on return of Z3_compute_interpolant and added interpolation example to test_capi.c 2016-02-11 16:09:54 -08:00
Nikolaj Bjorner
6c6da44f8f removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-02-09 22:24:37 +00:00
Nikolaj Bjorner
5ce85aba40 removing const qualifiers, perhaps this helps for #420 and adding assert to enable Clang analysis earlier for issue #440
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-02-09 22:23:37 +00:00
Christoph M. Wintersteiger
de3cb7e5dc More FPA exponent/siginficand order consistency 2016-01-05 18:05:21 +00:00
Dan Liew
83e2b1c6e5 Typo in comment in C api example. 2015-12-15 11:52:35 +00:00
Nikolaj Bjorner
995e112a18 fix examples
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-20 08:01:59 -08:00
Nikolaj Bjorner
90400ec914 update C example to use new API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-16 15:03:58 -08:00
Christoph M. Wintersteiger
88b027ecce Eliminated unused variable from C example. 2015-10-29 13:32:58 +00:00
Nikolaj Bjorner
d469a16bb8 add more Copyright notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-06-10 11:59:21 -07:00
Christoph M. Wintersteiger
48c72d2c38 FPA API: naming consistency
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-23 18:18:26 +00:00
Christoph M. Wintersteiger
1a6af4385e Fixed C example
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-21 15:01:50 +00:00
Christoph M. Wintersteiger
b46d76cddb New FPA C-API example
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-01 19:16:44 +00:00
Christoph M. Wintersteiger
261fe01cea FPA API bug and consistency fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-11-11 12:38:59 +00:00
Christoph M. Wintersteiger
8b40d4a735 FPA theory bug fixes.
Also removed unnecessary intermediate variables.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-08-04 17:00:04 +01:00
Christoph M. Wintersteiger
129e2f5e23 FPA API fixes and examples
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-06-11 17:55:31 +01:00
Christoph M. Wintersteiger
a8b65ebb36 added stubs for theory_fpa
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-04-23 20:10:53 +01: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
Leonardo de Moura
7f0fcefbe2 C examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-28 11:56:27 -07:00
Leonardo de Moura
91cc6bb768 renamed test_capi
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-28 10:51:50 -07:00