From d6a8803054c0c5731a6c4111d8d00c18e2953032 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 28 Oct 2019 12:50:08 -0500 Subject: Fix for non-linear models (#3410) * Towards fix for non-linear models * Format * Fix * More * Improve * Format * More --- test/regress/regress0/nl/issue3407.smt2 | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 test/regress/regress0/nl/issue3407.smt2 (limited to 'test/regress/regress0/nl') diff --git a/test/regress/regress0/nl/issue3407.smt2 b/test/regress/regress0/nl/issue3407.smt2 new file mode 100644 index 000000000..e4be74c8a --- /dev/null +++ b/test/regress/regress0/nl/issue3407.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic NRA) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun b () Real) +(assert (= (* a b) 1)) +(check-sat) -- cgit v1.2.3