mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-02 13:52:24 -07:00
parent 95493f78f9
commit e4b7b7bdf6
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/ba_solver.h
View file

@ -305,7 +305,7 @@ namespace sat {
unsigned_vector m_weights; unsigned_vector m_weights;
svector<wliteral> m_wlits; svector<wliteral> m_wlits;
euf::th_solver* ba_solver::fresh(sat::solver* new_s, ast_manager& m, sat::sat_internalizer& si, euf::theory_id id); euf::th_solver* fresh(sat::solver* new_s, ast_manager& m, sat::sat_internalizer& si, euf::theory_id id);
bool subsumes(card& c1, card& c2, literal_vector& comp); bool subsumes(card& c1, card& c2, literal_vector& comp);
bool subsumes(card& c1, clause& c2, bool& self); bool subsumes(card& c1, clause& c2, bool& self);