projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ac0c6de) | patch
Fix `TypeNode::substitute()` for type constants (#7920)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 11 Jan 2022 17:19:15 +0000 (09:19 -0800)
committerGitHub <noreply@github.com>
Tue, 11 Jan 2022 17:19:15 +0000 (17:19 +0000)
commit7ed586537b7767dee79a85e2754a12570328211c
treef6d6242dfa1905dd9b02eb69e46add060f91250ftree
parentac0c6dea9bac470813685dfb8dd12576fa20686fcommit | diff
Fix `TypeNode::substitute()` for type constants (#7920)

Fixes cvc5/cvc5-projects#395. The
TypeNode::substitute() method did not account for type constants such
as the Boolean type and was trying to use a NodeBuilder to build such
constants instead. This commit fixes the issue by adding a special case
for types without children.
src/expr/type_node.cpp diff | blob | history
test/api/cpp/CMakeLists.txt diff | blob | history
test/api/cpp/proj-issue395.cpp [new file with mode: 0644] blob