diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-19 19:34:18 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-19 19:34:18 -0500 |
| commit | 9712a20e6585728c7d0453e64e1e3b06a7d37b7f (patch) | |
| tree | b6941ff3df53fe92b0a1b9ea867c43ce2bb7d014 /test/regress/regress0/sygus | |
| parent | c8f149fa83fa16f821f37687fedfa778808809bd (diff) | |
Fix cached free variable identifiers in sygus term database (#4394)
Fixes an issue with over-pruning in SyGuS where using multiple sygus types that map to the same builtin type. Our mapping sygusToBuiltin did not ensure that free variables were unique.
Fixes #4383.
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/issue4383-cache-fv-id.sy | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/issue4383-cache-fv-id.sy b/test/regress/regress0/sygus/issue4383-cache-fv-id.sy new file mode 100644 index 000000000..27378d9ca --- /dev/null +++ b/test/regress/regress0/sygus/issue4383-cache-fv-id.sy @@ -0,0 +1,23 @@ +; EXPECT: unsat +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic ALL) +(synth-fun args_0_refinement_0 + ((r Int)) Bool + ((fv_B Bool)) + ( + (fv_B Bool (true)) + ) +) +(synth-fun ret_refinement_0 + ((x0 Int) (r Bool)) Bool + ((fv_B Bool) (B Bool) (I Int)) + ( + (fv_B Bool (r true (=> B fv_B))) + (B Bool ((Variable Bool) (= I I))) + (I Int ((Variable Int) 1)) + ) +) +(constraint (ret_refinement_0 1 true)) +(constraint (not (ret_refinement_0 1 false))) +(constraint (and (ret_refinement_0 0 false))) +(check-synth) |