mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
70b4822571
commit
1da7522893
|
@ -1323,7 +1323,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
|
||||
RETURN_Z3(nullptr);
|
||||
}
|
||||
SASSERT(mk_c(c)->m().contains(to_ast(a)));
|
||||
// yo! SASSERT(mk_c(c)->m().contains(to_ast(a)));
|
||||
ast_translation translator(mk_c(c)->m(), mk_c(target)->m());
|
||||
ast * _result = translator(to_ast(a));
|
||||
mk_c(target)->save_ast_trail(_result);
|
||||
|
|
|
@ -224,7 +224,7 @@ namespace api {
|
|||
|
||||
|
||||
void context::save_ast_trail(ast * n) {
|
||||
SASSERT(m().contains(n));
|
||||
// cherry on top? SASSERT(m().contains(n));
|
||||
if (m_user_ref_count) {
|
||||
// Corner case bug: n may be in m_last_result, and this is the only reference to n.
|
||||
// When, we execute reset() it is deleted
|
||||
|
|
|
@ -76,9 +76,9 @@ public:
|
|||
template<typename T>
|
||||
T * translate(T const * n) {
|
||||
if (&from() == &to()) return const_cast<T*>(n);
|
||||
SASSERT(!n || from().contains(const_cast<T*>(n)));
|
||||
// A Valentine? SASSERT(!n || from().contains(const_cast<T*>(n)));
|
||||
ast * r = process(n);
|
||||
SASSERT((!n && !r) || to().contains(const_cast<ast*>(r)));
|
||||
// Pretty please SASSERT((!n && !r) || to().contains(const_cast<ast*>(r)));
|
||||
return static_cast<T*>(r);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue