Sygus clean main (#1297)

* Remove front end hack for sygus.

* Remove other hack, add sygus solution output mode.

* Clang format

* Minor

* Fix

* Minor

* Remove unused field.

65 files changed, 65 insertions, 65 deletions

diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy
index cf0e37c9f..79b917c7a 100644
--- a/test/regress/regress0/expect/scrub.07.sy
+++ b/test/regress/regress0/expect/scrub.07.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (declare-var n Int)
 
diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 7f78dbc48..360474f84 100644
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
 ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM
diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy
index ee26fac79..1792749e2 100755
--- a/test/regress/regress0/sygus/General_plus10.sy
+++ b/test/regress/regress0/sygus/General_plus10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun fb () Int ((Start Int ((Constant Int)))))
diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy
index e6683ced9..41346e655 100644
--- a/test/regress/regress0/sygus/array_search_2.sy
+++ b/test/regress/regress0/sygus/array_search_2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy
index 387ce9487..84a75d086 100644
--- a/test/regress/regress0/sygus/array_sum_2_5.sy
+++ b/test/regress/regress0/sygus/array_sum_2_5.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress0/sygus/cegar1.sy b/test/regress/regress0/sygus/cegar1.sy
index dd7f73e27..ee85db88a 100644
--- a/test/regress/regress0/sygus/cegar1.sy
+++ b/test/regress/regress0/sygus/cegar1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth
+; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status
 (set-logic LIA)
 
 (synth-inv inv-f ((x Int) (y Int)))
diff --git a/test/regress/regress0/sygus/cggmp.sy b/test/regress/regress0/sygus/cggmp.sy
index 1ae1f53c0..a3247e4f4 100644
--- a/test/regress/regress0/sygus/cggmp.sy
+++ b/test/regress/regress0/sygus/cggmp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=pre --no-dump-synth
+; COMMAND-LINE: --sygus-inv-templ=pre --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy
index 2409b82d2..43fd7c1ac 100644
--- a/test/regress/regress0/sygus/clock-inc-tuple.sy
+++ b/test/regress/regress0/sygus/clock-inc-tuple.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 
 (set-logic ALL_SUPPORTED)
 (declare-var m Int)
diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy
index f675bddad..24201b453 100644
--- a/test/regress/regress0/sygus/commutative.sy
+++ b/test/regress/regress0/sygus/commutative.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
index b79b7eeec..305f5783a 100644
--- a/test/regress/regress0/sygus/const-var-test.sy
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy
index 5c48f5e39..1bb3e59fa 100644
--- a/test/regress/regress0/sygus/constant.sy
+++ b/test/regress/regress0/sygus/constant.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy
index 0a9fb9112..f4de9b055 100644
--- a/test/regress/regress0/sygus/dt-no-syntax.sy
+++ b/test/regress/regress0/sygus/dt-no-syntax.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 ; EXPECT: unsat
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy
index 0c28769b2..a6e8ac5c2 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=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy
index bed9972fd..e2c69282e 100644
--- a/test/regress/regress0/sygus/dup-op.sy
+++ b/test/regress/regress0/sygus/dup-op.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ Start Start) x))
diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy
index 7b59f5f1a..47099eeed 100644
--- a/test/regress/regress0/sygus/enum-test.sy
+++ b/test/regress/regress0/sygus/enum-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (define-sort D (Enum (a b)))
 (define-fun f ((x D)) Int (ite (= x D::a) 3 7))
diff --git a/test/regress/regress0/sygus/fg_polynomial3.sy b/test/regress/regress0/sygus/fg_polynomial3.sy
index dab92bb88..d70516bf1 100644
--- a/test/regress/regress0/sygus/fg_polynomial3.sy
+++ b/test/regress/regress0/sygus/fg_polynomial3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy
index 2e6c6ef81..1379d4206 100644
--- a/test/regress/regress0/sygus/hd-01-d1-prog.sy
+++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --cegqi --sygus-out=status
 
 (set-logic BV)
 
diff --git a/test/regress/regress0/sygus/icfp_14.12.sy b/test/regress/regress0/sygus/icfp_14.12.sy
index d9c19f8c1..51b86f0f5 100644
--- a/test/regress/regress0/sygus/icfp_14.12.sy
+++ b/test/regress/regress0/sygus/icfp_14.12.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy
index 74e054159..212ae37f5 100644
--- a/test/regress/regress0/sygus/icfp_28_10.sy
+++ b/test/regress/regress0/sygus/icfp_28_10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic BV)
 
diff --git a/test/regress/regress0/sygus/icfp_easy-ite.sy b/test/regress/regress0/sygus/icfp_easy-ite.sy
index 248264698..f0cbbdc53 100644
--- a/test/regress/regress0/sygus/icfp_easy-ite.sy
+++ b/test/regress/regress0/sygus/icfp_easy-ite.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy
index b56425964..ff68bc06c 100644
--- a/test/regress/regress0/sygus/inv-example.sy
+++ b/test/regress/regress0/sygus/inv-example.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-inv inv-f ((x Int) (y Int) (b Bool)))
 (declare-primed-var x Int)
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index d5d40ace4..d26edffd2 100644
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (synth-fun f ((x Int)) Int
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index d07f6a717..6f9d9fff9 100644
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int) (y Int)) Int
     ((Start Int (x
diff --git a/test/regress/regress0/sygus/list-head-x.sy b/test/regress/regress0/sygus/list-head-x.sy
index 8d209a9a0..6c5c1a97b 100644
--- a/test/regress/regress0/sygus/list-head-x.sy
+++ b/test/regress/regress0/sygus/list-head-x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic ALL_SUPPORTED)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy
index e6e3de5fc..37ed848ef 100644
--- a/test/regress/regress0/sygus/max.sy
+++ b/test/regress/regress0/sygus/max.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy
index 927148d81..0e00cfd9b 100644
--- a/test/regress/regress0/sygus/max2-univ.sy
+++ b/test/regress/regress0/sygus/max2-univ.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 ; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes)
 (set-logic LIA)
 (synth-fun max2 ((x Int) (y Int)) Int)
diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
index c238de5dd..22a2e0a4b 100644
--- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy
+++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy
index d3624a731..a1776cf93 100644
--- a/test/regress/regress0/sygus/nflat-fwd-3.sy
+++ b/test/regress/regress0/sygus/nflat-fwd-3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ (+ Con Con) Con) x))
diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy
index 3f15d5915..da26a6c93 100644
--- a/test/regress/regress0/sygus/nflat-fwd.sy
+++ b/test/regress/regress0/sygus/nflat-fwd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))
diff --git a/test/regress/regress0/sygus/nia-max-square-ns.sy b/test/regress/regress0/sygus/nia-max-square-ns.sy
index 96baab7fe..6e7f70ff0 100644
--- a/test/regress/regress0/sygus/nia-max-square-ns.sy
+++ b/test/regress/regress0/sygus/nia-max-square-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth --nl-ext-tplanes
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --nl-ext-tplanes
 (set-logic NIA)
 
 (synth-fun max ((x Int) (y Int)) Int)
diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy
index af1284f13..c0f0e4c0f 100644
--- a/test/regress/regress0/sygus/no-flat-simp.sy
+++ b/test/regress/regress0/sygus/no-flat-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-mention.sy b/test/regress/regress0/sygus/no-mention.sy
index 60efc1b74..f964d6039 100644
--- a/test/regress/regress0/sygus/no-mention.sy
+++ b/test/regress/regress0/sygus/no-mention.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun p ((x Int) (y Int)) Int)
diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy
index ee27b30eb..c6c9383bb 100644
--- a/test/regress/regress0/sygus/no-syntax-test-bool.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
index bd8da1900..8f333811c 100644
--- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy
index 2b3d5f3e9..f27a07ee7 100644
--- a/test/regress/regress0/sygus/no-syntax-test.sy
+++ b/test/regress/regress0/sygus/no-syntax-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
index 3cc577bd8..50c7d39a0 100644
--- a/test/regress/regress0/sygus/parity-AIG-d0.sy
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
diff --git a/test/regress/regress0/sygus/parse-bv-let.sy b/test/regress/regress0/sygus/parse-bv-let.sy
index 88ddcf139..1329918fc 100644
--- a/test/regress/regress0/sygus/parse-bv-let.sy
+++ b/test/regress/regress0/sygus/parse-bv-let.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
diff --git a/test/regress/regress0/sygus/qe.sy b/test/regress/regress0/sygus/qe.sy
index eaff0fd9a..5661f4469 100644
--- a/test/regress/regress0/sygus/qe.sy
+++ b/test/regress/regress0/sygus/qe.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f ((x Int)) Int)
diff --git a/test/regress/regress0/sygus/strings-concat-3-args.sy b/test/regress/regress0/sygus/strings-concat-3-args.sy
index 3c93c51d3..6628ff746 100644
--- a/test/regress/regress0/sygus/strings-concat-3-args.sy
+++ b/test/regress/regress0/sygus/strings-concat-3-args.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((x String)) String
 ((Start String (ntString))
diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy
index 40346bcdf..7d976ff39 100644
--- a/test/regress/regress0/sygus/strings-small.sy
+++ b/test/regress/regress0/sygus/strings-small.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((firstname String) (lastname String)) String
 ((Start String (ntString))
diff --git a/test/regress/regress0/sygus/strings-template-infer.sy b/test/regress/regress0/sygus/strings-template-infer.sy
index 498e713e8..13c4d7dac 100644
--- a/test/regress/regress0/sygus/strings-template-infer.sy
+++ b/test/regress/regress0/sygus/strings-template-infer.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
  
 (define-fun cA ((x String) (y String)) String (str.++ (str.++ x "A") y))
diff --git a/test/regress/regress0/sygus/strings-trivial-simp.sy b/test/regress/regress0/sygus/strings-trivial-simp.sy
index d37ac8bf4..f5e41a8f5 100644
--- a/test/regress/regress0/sygus/strings-trivial-simp.sy
+++ b/test/regress/regress0/sygus/strings-trivial-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
  
 (synth-fun f ((name String)) String
diff --git a/test/regress/regress0/sygus/strings-trivial.sy b/test/regress/regress0/sygus/strings-trivial.sy
index f4847922d..9af0a1bb1 100644
--- a/test/regress/regress0/sygus/strings-trivial.sy
+++ b/test/regress/regress0/sygus/strings-trivial.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
  
 (synth-fun f ((name String)) String
diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy
index 38e69e337..39c392487 100644
--- a/test/regress/regress0/sygus/strings-unconstrained.sy
+++ b/test/regress/regress0/sygus/strings-unconstrained.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((firstname String) (lastname String)) String
 ((Start String (ntString))
diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy
index 59560ed61..d496e3fdc 100644
--- a/test/regress/regress0/sygus/sygus-dt.sy
+++ b/test/regress/regress0/sygus/sygus-dt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/tl-type-0.sy b/test/regress/regress0/sygus/tl-type-0.sy
index ef046c8e0..ceda89d78 100644
--- a/test/regress/regress0/sygus/tl-type-0.sy
+++ b/test/regress/regress0/sygus/tl-type-0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Term Term)))
diff --git a/test/regress/regress0/sygus/tl-type-4x.sy b/test/regress/regress0/sygus/tl-type-4x.sy
index a18d13052..bf8eee5ee 100644
--- a/test/regress/regress0/sygus/tl-type-4x.sy
+++ b/test/regress/regress0/sygus/tl-type-4x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int (Term (+ Start Start)))
diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy
index a6980425a..6f25a570e 100644
--- a/test/regress/regress0/sygus/tl-type.sy
+++ b/test/regress/regress0/sygus/tl-type.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int (Term (+ Start Start)))
diff --git a/test/regress/regress0/sygus/triv-type-mismatch-si.sy b/test/regress/regress0/sygus/triv-type-mismatch-si.sy
index e2935af51..37c5a7f53 100644
--- a/test/regress/regress0/sygus/triv-type-mismatch-si.sy
+++ b/test/regress/regress0/sygus/triv-type-mismatch-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun R ((y Int)) Bool)
diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy
index b016872b4..06d2ecb71 100644
--- a/test/regress/regress0/sygus/twolets1.sy
+++ b/test/regress/regress0/sygus/twolets1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 ;; f1 is x plus 2 ;; f2 is 2x plus 5
diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy
index 70d1ffa02..50f7ad544 100644
--- a/test/regress/regress0/sygus/twolets2-orig.sy
+++ b/test/regress/regress0/sygus/twolets2-orig.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun f1 ((x Int)) Int
      (
diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy
index e98be942b..94040bf45 100644
--- a/test/regress/regress0/sygus/uminus_one.sy
+++ b/test/regress/regress0/sygus/uminus_one.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
 (declare-var x Int)
diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
index 300b6b65c..d45cec38b 100644
--- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
+++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 (synth-fun inv ((x Int)) Bool
diff --git a/test/regress/regress1/sygus/MPwL_d1s3.sy b/test/regress/regress1/sygus/MPwL_d1s3.sy
index b5b848848..5178cf86b 100644
--- a/test/regress/regress1/sygus/MPwL_d1s3.sy
+++ b/test/regress/regress1/sygus/MPwL_d1s3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth 
+; COMMAND-LINE: --sygus-out=status 
 (set-logic LIA)
 
 (define-fun get-y ((currPoint Int)) Int 
diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy
index 75bed6a28..32e4723aa 100644
--- a/test/regress/regress1/sygus/VC22_a.sy
+++ b/test/regress/regress1/sygus/VC22_a.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f ((x1 Int) (x2 Int)) Int
diff --git a/test/regress/regress1/sygus/array_sum_dd.sy b/test/regress/regress1/sygus/array_sum_dd.sy
index dacd7347d..6d3354d2d 100644
--- a/test/regress/regress1/sygus/array_sum_dd.sy
+++ b/test/regress/regress1/sygus/array_sum_dd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int (
 (Start Int ( 0 1 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) 
diff --git a/test/regress/regress1/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy
index 019b48a1c..37e1daf88 100644
--- a/test/regress/regress1/sygus/hd-sdiv.sy
+++ b/test/regress/regress1/sygus/hd-sdiv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic BV)
 
 (define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001))
diff --git a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy b/test/regress/regress1/sygus/icfp_easy_mt_ite.sy
index b7428fd51..799633fa3 100644
--- a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy
+++ b/test/regress/regress1/sygus/icfp_easy_mt_ite.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
diff --git a/test/regress/regress1/sygus/inv_gen_fig8.sy b/test/regress/regress1/sygus/inv_gen_fig8.sy
index 5496f3c0a..19c36e4dc 100644
--- a/test/regress/regress1/sygus/inv_gen_fig8.sy
+++ b/test/regress/regress1/sygus/inv_gen_fig8.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((l Int)) Bool
     (
diff --git a/test/regress/regress1/sygus/inv_gen_n_c11.sy b/test/regress/regress1/sygus/inv_gen_n_c11.sy
index 946f284cb..9e04682a5 100644
--- a/test/regress/regress1/sygus/inv_gen_n_c11.sy
+++ b/test/regress/regress1/sygus/inv_gen_n_c11.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((i Int) (l Int)) Bool
     (
diff --git a/test/regress/regress1/sygus/mpg_guard1-dd.sy b/test/regress/regress1/sygus/mpg_guard1-dd.sy
index e574f7eb6..31800a36f 100644
--- a/test/regress/regress1/sygus/mpg_guard1-dd.sy
+++ b/test/regress/regress1/sygus/mpg_guard1-dd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun eq1 ( (x Int) (y Int) ) Int
diff --git a/test/regress/regress1/sygus/nia-max-square.sy b/test/regress/regress1/sygus/nia-max-square.sy
index 5858af98a..e023e837b 100644
--- a/test/regress/regress1/sygus/nia-max-square.sy
+++ b/test/regress/regress1/sygus/nia-max-square.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth --nl-ext-tplanes
+; COMMAND-LINE: --sygus-out=status --nl-ext-tplanes
 (set-logic NIA)
 
 (synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress1/sygus/stopwatch-bt.sy b/test/regress/regress1/sygus/stopwatch-bt.sy
index 016280521..291ae6099 100644
--- a/test/regress/regress1/sygus/stopwatch-bt.sy
+++ b/test/regress/regress1/sygus/stopwatch-bt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth
+; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status
 (set-logic LIA)
 
 (define-fun
diff --git a/test/regress/regress1/sygus/three.sy b/test/regress/regress1/sygus/three.sy
index 6e2ce3a2c..831e5beb1 100644
--- a/test/regress/regress1/sygus/three.sy
+++ b/test/regress/regress1/sygus/three.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth 
+; COMMAND-LINE: --sygus-out=status 
 
 (set-logic LIA)
 
diff --git a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
index f840fa519..73d410d51 100644
--- a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
+++ b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((i Int) (y Int) (l Int)) Bool
     (