diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-06 09:24:11 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-06 09:24:11 -0600 |
| commit | 210e6db5c6a76ee1e554426058ecf3397575f1e3 (patch) | |
| tree | 98140a04acd9eedc91e2d598224ac7005d0a3540 /test/regress/regress0/sygus | |
| parent | a727f6314c8f2ad72d8d83eb63c413bab68d1b08 (diff) | |
Support default sygus grammar construction for sets (#3842)
Fixes #3645.
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/issue3645-grammar-sets.smt2 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/issue3645-grammar-sets.smt2 b/test/regress/regress0/sygus/issue3645-grammar-sets.smt2 new file mode 100644 index 000000000..22a5e07d4 --- /dev/null +++ b/test/regress/regress0/sygus/issue3645-grammar-sets.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +; COMMAND-LINE: --sygus-inference +(set-logic ALL) +(declare-fun a () (Set (_ BitVec 2))) +(declare-fun b () (Set (_ BitVec 2))) +(assert (= a b)) +(check-sat) |