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

comment typos

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-31 16:14:50 +01:00
parent 39acd3594a
commit 03f6b465b9
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/act_cache.cpp
View file

@ -40,7 +40,7 @@ Notes:
The number of unused entries (m_unused) is equal to the number of entries
of the form
t -> (s, 0)
That is, it is the number of keys that were never accessed by cliend code.
That is, it is the number of keys that were never accessed by client code.
The cache maintains at most m_max_unused entries.
When the maximum number of unused entries exceeds m_max_unused, then

8
src/smt/smt_internalizer.cpp
View file

@ -656,10 +656,10 @@ namespace smt {
/**
\brief Enable the flag m_merge_tf in the given enode. When the
flag m_merge_tf is enabled, the enode n will be merged with the
true_enode (false_enode) whenever the boolean variable v is
true_enode (false_enode) whenever the Boolean variable v is
assigned to true (false).
If is_new_var is true, then trail is not created for the flag uodate.
If is_new_var is true, then trail is not created for the flag update.
*/
void context::set_merge_tf(enode * n, bool_var v, bool is_new_var) {
SASSERT(bool_var2enode(v) == n);
@ -674,8 +674,8 @@ namespace smt {
}
/**
\brief Trail object to disable the m_enode flag of a boolean
variable. The flag m_enode is true for a boolean variable v,
\brief Trail object to disable the m_enode flag of a Boolean
variable. The flag m_enode is true for a Boolean variable v,
if there is an enode n associated with it.
*/
class set_enode_flag_trail : public trail<context> {