From 0e09af0be57ec4df28869e4383a40d847c0a6b5a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 9 Mar 2020 22:18:58 -0500 Subject: Rename sygus option name (#3977) This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach). It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason. --- test/regress/regress1/sygus/hd-01-d1-prog.sy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress1') diff --git a/test/regress/regress1/sygus/hd-01-d1-prog.sy b/test/regress/regress1/sygus/hd-01-d1-prog.sy index 1379d4206..bbdbda1bd 100644 --- a/test/regress/regress1/sygus/hd-01-d1-prog.sy +++ b/test/regress/regress1/sygus/hd-01-d1-prog.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --sygus-out=status +; COMMAND-LINE: --sygus-out=status (set-logic BV) -- cgit v1.2.3