From 2e02c1c2fb999f2f1cdefe867f843c2c46ad0ef0 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 18 May 2016 10:06:49 -0500 Subject: Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Minor fixes for inst max level. --- test/regress/regress0/sygus/dt-test-ns.sy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress0/sygus/dt-test-ns.sy') diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy index ed17f4ff2..052065061 100644 --- a/test/regress/regress0/sygus/dt-test-ns.sy +++ b/test/regress/regress0/sygus/dt-test-ns.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si --no-dump-synth +; COMMAND-LINE: --cegqi-si=all --no-dump-synth (set-logic LIA) (declare-datatypes () ((List (cons (head Int) (tail List)) (nil)))) -- cgit v1.2.3