From 1cd3c3c5dad84093aa6b2db164798c8fff473fec Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Jul 2020 01:41:24 -0500 Subject: Debug instantiations output (#4739) This prints # instantiations per round (during solving) for each quantified formula with `--debug-inst`, giving output like this: ``` (num-instantiations myQuant1 1) (num-instantiations myQuant2 1) unsat ``` It also changes the default value of print-inst-full to match the behavior of unsat-cores vs unsat-cores-full (by default, nameless quantifiers are ignored). It fixes an issue with qid, where mkVar was accidentally used instead of mkConst, leading to assertion failures in debug. Marking major since this fixes debug regress1. --- src/parser/smt2/Smt2.g | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/parser') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 62ea4e4fa..b88dc70b6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1901,7 +1901,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr] { api::Sort boolType = SOLVER->getBooleanSort(); - api::Term avar = SOLVER->mkVar(boolType, sexpr.toString()); + api::Term avar = SOLVER->mkConst(boolType, sexpr.toString()); attr = std::string(":qid"); retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); Command* c = new SetUserAttributeCommand("qid", avar.getExpr()); -- cgit v1.2.3