Steven Moy
111fcb9366
Implement API to set exit action to exception ( #7192 )
...
* Implement API to set exit action to exception
* Turn on exit_action_to_throw_exception upon API context creation
2024-03-27 19:06:58 -07:00
Jakob Rath
d69155b9e9
Shared features from polysat branch ( #6567 )
...
* Allow setting default debug action
* Fix dlist and add iterator
* Add var_queue iterator
* Add some helpers
* rational: machine_div2k and pseudo_inverse
* Basic support for non-copyable types in map
* tbv helpers
* pdd updates
* Remove duplicate functions
gcc doesn't like having both versions
2023-02-03 13:08:47 -08:00
Jakob Rath
d2fe174320
Add SASSERT_EQ and VERIFY_EQ
2022-08-01 18:37:11 +03:00
Nikolaj Bjorner
797f50e699
DRAT debugging updates
2020-11-22 15:38:57 -08:00
Nuno Lopes
d8cea7c8d5
fix a few warnings & simplify debug.h header
2020-05-26 13:49:13 +01:00
Daniel Peebles
7e34925035
Improve UX for unreachable/unimplemented errors ( #4094 )
...
This should replace several "segfaults" and "illegal instruction" errors
with messages that contain a bit more context. I also put in a link to
the bug tracker to make users' lives a bit easier.
For context, `__builtin_unreachable`'s behavior is undefined and is
intended only as a mechanism to help the compiler see that code will not
return. I do still include it in the new code because if I don't,
compilation produces a lot more warnings as it can't see that
`NOT_IMPLEMENTED_YET` and `UNREACHABLE` cannot return.
2020-04-28 19:54:31 -07:00
Lev Nachmanson
3441f565b2
before changes is basic_sign_lemma
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Lev Nachmanson
1230b46008
perf in equiv_monomials
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
Bruce Mitchener
d757c342d5
Define NO_Z3_DEBUGGER for emscripten builds.
2019-01-07 23:13:09 +07:00
Bruce Mitchener
7e1ce2a16c
Define NO_Z3_DEBUGGER for iOS builds.
...
This is defined because we can't call `system` (via `invoke_gdb`)
on iOS and related platforms.
2019-01-06 12:16:33 +07:00
Nikolaj Bjorner
cae414e575
fixes for #1296 , removing COMPILE_TIME_ASSERT
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-09 13:59:44 -07:00
Nuno Lopes
632c2d8ebf
use static_assert in COMPILE_TIME_ASSERT
2017-08-14 20:10:17 +01:00
Nikolaj Bjorner
b19f94ae5b
make include paths uniformly use path relative to src. #534
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
b1298d7bde
ensure that assertions within the unit tests are exercised in all build modes, remove special handling of SASSERT for release mode #1163
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-26 20:28:55 -07:00
Christoph M. Wintersteiger
e53b580cb4
added compiler macro to disable invocation of the debugger upon failure.
2016-01-07 15:58:10 +00:00
Nuno Lopes
d9bafc3fba
rewrite scoped_timer for linux
...
The previous version was racy and could lead to crashes.
The timer could be deleted before the callback was called, making it execute on already freed memory
This new version is similar to Mac's. It spawns its own thread and uses pthread_cond_wait.
Care is taken for small timeouts to avoid races in the thread creation and timer destruction.
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-11-22 11:40:52 +00:00
Nikolaj Bjorner
4bc044c982
update header guards to be C++ style. Fixes issue #9
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Nuno Lopes
9d5bc024e4
add implementation of UNREACHABLE for MSVC in release mode.
...
This reduces code size of Z3 by 0.1% \o/
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
2015-02-05 09:51:05 +00:00
Nuno Lopes
61d67dc2de
fix a few compiler warnings
...
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
2014-09-18 14:38:40 +01:00
Nuno Lopes
7ce88d4da9
fix a few compilation warnings
...
- remove unused variables and class fields
- add support for gcc 4.5 & clang's __builtin_unreachable
- fix 2 bugs related to strict aliasing
- remove a few unused function parameters
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-21 14:36:39 -07:00
Leonardo de Moura
e0c79c06bc
removed class
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-22 15:21:57 -08:00
Leonardo de Moura
ed5d154f78
broke dependency between components that need initialization and memory_manager
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-17 11:30:25 -08:00
Leonardo de Moura
d8f627c6c8
Fixed warnings produced by gcc 4.6.3 when compiling in debug mode
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-30 23:43:00 -07:00
Leonardo de Moura
2c464d413d
Reorganizing source code. Created util dir
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-20 10:19:38 -07:00
