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/regress/regress1/quantifiers | |
| 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/regress/regress1/quantifiers')
| -rw-r--r-- | test/regress/regress1/quantifiers/horn-simple.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
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) |