diff --git a/Makefile b/Makefile index 7db5cc728..fb36ab4a9 100644 --- a/Makefile +++ b/Makefile @@ -169,7 +169,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.51+17 +YOSYS_VER := 0.51+46 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2) diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 3b089ccca..20a210abe 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -676,10 +676,10 @@ void ezSAT::preSolverCallback() bool ezSAT::solver(const std::vector&, std::vector&, const std::vector&) { preSolverCallback(); - fprintf(stderr, "************************************************************************\n"); - fprintf(stderr, "ERROR: You are trying to use the solve() method of the ezSAT base class!\n"); + fprintf(stderr, "*************************************************************************\n"); + fprintf(stderr, "ERROR: You are trying to use the solver() method of the ezSAT base class!\n"); fprintf(stderr, "Use a dervied class like ezMiniSAT instead.\n"); - fprintf(stderr, "************************************************************************\n"); + fprintf(stderr, "*************************************************************************\n"); abort(); } @@ -1332,7 +1332,7 @@ void ezSAT::printInternalState(FILE *f) const fprintf(f, "\n"); } if (cnfConsumed) - fprintf(f, " *** more clauses consumed via cnfConsume() ***\n"); + fprintf(f, " *** more clauses consumed via consumeCnf() ***\n"); fprintf(f, "--8<-- snap --8<--\n"); } diff --git a/passes/opt/share.cc b/passes/opt/share.cc index 57a52969b..dfc44758f 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -1325,8 +1325,8 @@ struct ShareWorker qcsat.ez->assume(qcsat.ez->AND(sub1, sub2)); - log(" Size of SAT problem: %d variables, %d clauses\n", - qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses()); + log(" Size of SAT problem: %zu cells, %d variables, %d clauses\n", + qcsat.imported_cells.size(), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses()); if (qcsat.ez->solve(sat_model, sat_model_values)) { log(" According to the SAT solver this pair of cells can not be shared.\n");