mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

update

Browse source
This commit is contained in:
comet 2020-01-27 17:12:06 -06:00 • committed by Nikolaj Bjorner
parent d12523e4c0
commit eea7805551
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -668,7 +668,7 @@ ast* ast_table::pop_erase() {
// ----------------------------------- // -----------------------------------
/** /**
\brief Checks wether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line \brief Checks whether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line
to that log. The theory solver should add some description of the meaning of the term in terms of the theory's to that log. The theory solver should add some description of the meaning of the term in terms of the theory's
internal reasoning to the end of the line and insert a line break. internal reasoning to the end of the line and insert a line break.

2
src/ast/ast.h
View file

@ -1004,7 +1004,7 @@ protected:
virtual void inherit(decl_plugin* other_p, ast_translation& ) { } virtual void inherit(decl_plugin* other_p, ast_translation& ) { }
/** /**
\brief Checks wether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line \brief Checks whether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line
to that log. The theory solver should add some description of the meaning of the term in terms of the theory's to that log. The theory solver should add some description of the meaning of the term in terms of the theory's
internal reasoning to the end of the line and insert a line break. internal reasoning to the end of the line and insert a line break.