projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 9557a5b)
Fix option for real2int regression. (#2353)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 22 Aug 2018 17:39:22 +0000 (12:39 -0500)
committerGitHub <noreply@github.com>
Wed, 22 Aug 2018 17:39:22 +0000 (12:39 -0500)
test/regress/regress1/arith/real2int-test.smt2 patch | blob | history

diff --git a/test/regress/regress1/arith/real2int-test.smt2 b/test/regress/regress1/arith/real2int-test.smt2
index 77bc1eda2f6e2a7a8041f963e49a387303479884..a769aa4de117a3fd5ccfe7e75f938f28c6bc2249 100644 (file)
--- a/test/regress/regress1/arith/real2int-test.smt2
+++ b/test/regress/regress1/arith/real2int-test.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-real-as-int
+; COMMAND-LINE: --solve-real-as-int --no-new-prop
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic QF_NRA)