mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

#5261

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-10 13:35:25 -07:00
parent 897a2d6470
commit d27d09f87a
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/shell/dimacs_frontend.cpp
View file

@ -66,6 +66,7 @@ static void STD_CALL on_ctrl_c(int) {
static void display_model(sat::solver const & s) {
sat::model const & m = s.get_model();
std::cout << "v ";
for (unsigned i = 1; i < m.size(); i++) {
switch (m[i]) {
case l_false: std::cout << "-" << i << " "; break;
@ -77,7 +78,7 @@ static void display_model(sat::solver const & s) {
}
static void display_core(sat::solver const& s, vector<sat::literal_vector> const& tracking_clauses) {
std::cout << "core\n";
std::cout << "v core\n";
sat::literal_vector const& c = s.get_core();
for (unsigned i = 0; i < c.size(); ++i) {
sat::literal_vector const& cls = tracking_clauses[c[i].var()];