summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/printer/printer.h2
-rw-r--r--src/printer/smt2/smt2_printer.cpp2
-rw-r--r--src/printer/smt2/smt2_printer.h13
-rw-r--r--src/smt/command.cpp3
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/sygus/issue5512-vvv.sy17
6 files changed, 29 insertions, 9 deletions
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 068c79330..bfc1dc64a 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -135,7 +135,7 @@ class Printer
const std::vector<Node>& vars,
TypeNode range,
bool isInv,
- TypeNode sygusType) const;
+ TypeNode sygusType = TypeNode::null()) const;
/** Print constraint command */
virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 376913ebd..81445d281 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -2043,7 +2043,7 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
}
out << '\n';
// print grammar, if any
- if (sygusType != TypeNode::null())
+ if (!sygusType.isNull())
{
toStreamSygusGrammar(out, sygusType);
}
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 287a81286..1e6be22d3 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -117,12 +117,13 @@ class Smt2Printer : public CVC4::Printer
TypeNode type) const override;
/** Print synth-fun command */
- void toStreamCmdSynthFun(std::ostream& out,
- const std::string& sym,
- const std::vector<Node>& vars,
- TypeNode range,
- bool isInv,
- TypeNode sygusType) const override;
+ void toStreamCmdSynthFun(
+ std::ostream& out,
+ const std::string& sym,
+ const std::vector<Node>& vars,
+ TypeNode range,
+ bool isInv,
+ TypeNode sygusType = TypeNode::null()) const override;
/** Print constraint command */
void toStreamCmdConstraint(std::ostream& out, Node n) const override;
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index cfd25fa3b..2a316409e 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -689,7 +689,8 @@ void SynthFunCommand::toStream(std::ostream& out,
nodeVars,
d_sort.getTypeNode(),
d_isInv,
- d_grammar->resolve().getTypeNode());
+ d_grammar == nullptr ? TypeNode::null()
+ : d_grammar->resolve().getTypeNode());
}
/* -------------------------------------------------------------------------- */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 56780278b..ef00b11b0 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1091,6 +1091,7 @@ set(regress_0_tests
regress0/sygus/issue3645-grammar-sets.smt2
regress0/sygus/issue4383-cache-fv-id.sy
regress0/sygus/issue4790-dtd.sy
+ regress0/sygus/issue5512-vvv.sy
regress0/sygus/let-ringer.sy
regress0/sygus/let-simp.sy
regress0/sygus/no-logic.sy
diff --git a/test/regress/regress0/sygus/issue5512-vvv.sy b/test/regress/regress0/sygus/issue5512-vvv.sy
new file mode 100644
index 000000000..9d37032ac
--- /dev/null
+++ b/test/regress/regress0/sygus/issue5512-vvv.sy
@@ -0,0 +1,17 @@
+; COMMAND-LINE: -vvv --sygus-out=status --check-synth-sol --check-abducts
+; SCRUBBER: sed -e 's/.*//g'
+; EXIT: 0
+
+; This regression ensures that printing Sygus commands with option -vvv does not
+; crash CVC4
+
+(set-logic UF)
+(declare-var x Bool)
+(synth-fun f ((x Bool)) Bool ((Start Bool)) ((Start Bool (true))))
+(synth-inv inv-f ((x Bool)))
+(define-fun pre-f ((x Bool)) Bool true)
+(define-fun trans-f ((x Bool) (x! Bool)) Bool true)
+(define-fun post-f ((x Bool)) Bool true)
+(inv-constraint inv-f pre-f trans-f post-f)
+(constraint true)
+(check-synth)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback