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

fix

Browse source
This commit is contained in:
Jakob Rath 2023-02-03 15:59:26 +01:00
parent 6365e322f3
commit 63416dbcd7
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/boolean.h
View file

@ -70,6 +70,7 @@ namespace polysat {
dependency dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
ptr_vector<clause>& watch(sat::literal lit) { return m_watch[lit.index()]; }
ptr_vector<clause> const& watch(sat::literal lit) const { return m_watch[lit.index()]; }
/// Set the given literal to true
void propagate(sat::literal lit, unsigned lvl, clause& reason);