diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-09-16 20:34:40 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-16 22:34:40 -0500 |
| commit | 14041ad14583f670bc03d5eef6535544d86fc9fc (patch) | |
| tree | f81b8503c7e0eae4431535241de2acd37f2f0fa6 /test/regress/regress0/print_define_fun_internal.smt2 | |
| parent | 70bfc4f67bcad32fa1b9b581b71b3a2d70e14d7e (diff) | |
Dumping internal define-funs with no arguments (#5077)
Currently, --dump=assertions:... fails if a define-fun command is executed internally (an example for this can be found here.
The failure occurs because the printer expects a range type whenever a define-fun command is executed. However, when this command is used for 0-ary functions (variables), the getter for the range fails.
This PR fixes this by asking for a range only if the type is indeed a function. Otherwise, the original type is printed.
A test that currently fails but passes with this PR is included.
Diffstat (limited to 'test/regress/regress0/print_define_fun_internal.smt2')
| -rw-r--r-- | test/regress/regress0/print_define_fun_internal.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/print_define_fun_internal.smt2 b/test/regress/regress0/print_define_fun_internal.smt2 new file mode 100644 index 000000000..22665d54c --- /dev/null +++ b/test/regress/regress0/print_define_fun_internal.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --solve-real-as-int --dump=assertions:post-real-to-int +; EXIT: 0 +; SCRUBBER: grep -v -E '.*' +(set-logic QF_NRA) +(declare-fun a () Real) +(declare-fun b () Real) +(assert (= (* a a) 4)) +(assert (= (* b b) 0)) +(assert (= (+ (* a a) (* b b)) 4)) +(check-sat) |