Remove spurious assertion involving constants for arguments to UF from FMF (#8168)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 25 Feb 2022 16:27:16 +0000 (10:27 -0600)
committerGitHub <noreply@github.com>
Fri, 25 Feb 2022 16:27:16 +0000 (16:27 +0000)
commit81412133512647fed893dc8f0a6cfdbe09d407da
tree1a26e4b1caba05778ed3726dc9a4b594f3c38137
parent31852631ba7fb56eac1f4a74df1ffd71735af272
Remove spurious assertion involving constants for arguments to UF from FMF (#8168)

Fixes #8163.
src/theory/quantifiers/fmf/full_model_check.cpp
test/regress/CMakeLists.txt
test/regress/regress1/fmf/issue8163-nconst-arg.smt2 [new file with mode: 0644]