projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9d563b2) | patch
Fixes for sygus-rr-synth-input (#7716)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 2 Dec 2021 17:12:10 +0000 (11:12 -0600)
committerGitHub <noreply@github.com>
Thu, 2 Dec 2021 17:12:10 +0000 (17:12 +0000)
commit4270c3d6b8fa45e66a79c928267a0757954d8004
treece94eadad454d448cf0da2e42d5b1c9cca5ac0d2tree
parent9d563b2963835b2a4e6ab19bdf5a5b21d934416ecommit | diff
Fixes for sygus-rr-synth-input (#7716)

Includes aborting when no non-constant subterms exist, a spurious assertion failure, and bad variable names.

Fixes cvc5/cvc5-projects#351

Fixes cvc5/cvc5-projects#353
src/preprocessing/passes/synth_rew_rules.cpp diff | blob | history