diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-22 10:02:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-22 15:02:05 +0000 |
| commit | ccd0e7fdf1484d72b0a2565fefd0259fe7557b0c (patch) | |
| tree | 5713dd6c821f13151e6ba71f519d5d2394a316c6 /test | |
| parent | bc928d24d7454d81f39006b4129a29286fcd10eb (diff) | |
Fix models for sygus-inference, bv2int, real2int (#6421)
In each case, previously we were generating a define-fun, what we needed was to do a model substitution.
This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.
Diffstat (limited to 'test')
4 files changed, 5 insertions, 3 deletions
diff --git a/test/regress/regress0/push-pop/real-as-int-incremental.smt2 b/test/regress/regress0/push-pop/real-as-int-incremental.smt2 index 81af8c4e7..155033d7d 100644 --- a/test/regress/regress0/push-pop/real-as-int-incremental.smt2 +++ b/test/regress/regress0/push-pop/real-as-int-incremental.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --solve-real-as-int +; COMMAND-LINE: --incremental --solve-real-as-int -q ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat diff --git a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 index 082df249b..3a4f24521 100644 --- a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 +++ b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-inference +; COMMAND-LINE: --sygus-inference -q ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2 index b851d2e19..d333358ed 100644 --- a/test/regress/regress1/quantifiers/horn-simple.smt2 +++ b/test/regress/regress1/quantifiers/horn-simple.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer +; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer -q ; EXPECT: sat (set-logic UFLIA) (set-info :status sat) diff --git a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 index 471cc519b..6d0b37a30 100644 --- a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 +++ b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic ALL) (set-option :conjecture-filter-model true) (set-option :conjecture-gen true) |