diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-19 17:40:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-19 17:40:33 -0500 |
| commit | e1fcbe514b5876b95ff93b5248e6a9f786ddbd1c (patch) | |
| tree | 84cadc958ae96fdfa3fff4fc22d782e0a225340c /test/regress/regress0/use_approx | |
| parent | 68d7289ab38f0381bed60ee852175f26bb20d1d2 (diff) | |
| parent | 09719301db1532093117bc60546e01dca77b59b8 (diff) | |
Merge branch 'master' into rmNoInteractivePromptrmNoInteractivePrompt
Diffstat (limited to 'test/regress/regress0/use_approx')
| -rw-r--r-- | test/regress/regress0/use_approx/bug812_approx.smt2 | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress0/use_approx/bug812_approx.smt2 b/test/regress/regress0/use_approx/bug812_approx.smt2 index 4b5af6710..45908e3dd 100644 --- a/test/regress/regress0/use_approx/bug812_approx.smt2 +++ b/test/regress/regress0/use_approx/bug812_approx.smt2 @@ -1,11 +1,10 @@ ; REQUIRES: glpk ; COMMAND-LINE: --use-approx -; EXPECT: unknown (set-logic UFNIA) (set-info :source "Reduced from regression 'bug812.smt2' using ddSMT to exercise GLPK") (set-info :smt-lib-version 2.6) (set-info :category "crafted") -(set-info :status unknown) +(set-info :status unsat) (declare-fun s (Int Int) Int) (declare-fun P (Int Int Int) Int) (declare-fun p (Int) Int) |