Ensure variables are constrained in model when equal to transcendental function apps...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 24 Feb 2022 23:56:33 +0000 (17:56 -0600)
committerGitHub <noreply@github.com>
Thu, 24 Feb 2022 23:56:33 +0000 (23:56 +0000)
commitb8b52b5cfa2fbfcb6d3450b9e03b2fa680af605d
tree19ad4d232890fecc9c799f5674f226a4dd176353
parentc7e68b150858560656ee2fd557cd8358842b03c9
Ensure variables are constrained in model when equal to transcendental function apps (#8153)

Fixes #8147.
src/smt/check_models.cpp
src/theory/arith/nl/transcendental/transcendental_solver.cpp
src/theory/arith/nl/transcendental/transcendental_solver.h
test/regress/CMakeLists.txt
test/regress/regress0/nl/nta/issue8147-unc-model.smt2 [new file with mode: 0644]