projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ab8a3a) | patch
Fix a bug with synth-fun printer (#5512)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Tue, 8 Dec 2020 20:10:10 +0000 (14:10 -0600)
committerGitHub <noreply@github.com>
Tue, 8 Dec 2020 20:10:10 +0000 (14:10 -0600)
commit3255e4335f25f35318a41f174ec15a28b0f0520d
treecc79f2a3f325167d3210a1d89e2114e369cf6282tree
parent0ab8a3a7af5b80aa7bcaa028276cdc396aa7a4cbcommit | diff
Fix a bug with synth-fun printer (#5512)

This PR fixes #5448. SynthFunCommand::toStream used to call d_grammar->resolve even when d_grammar is a nullptr. This PR fixes the issue and modifies the signature of Printer::toStreamCmdSynthFun to make it clear that grammar is an optional argument.
src/printer/printer.h diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.h diff | blob | history
src/smt/command.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/issue5512-vvv.sy [new file with mode: 0644] blob