16 files changed, 232 insertions, 404 deletions
diff --git a/test/regress/regress2/bv_to_int2.smt2 b/test/regress/regress2/bv_to_int2.smt2
index 424e95b27..b9c27c6b8 100644
--- a/test/regress/regress2/bv_to_int2.smt2
+++ b/test/regress/regress2/bv_to_int2.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index 0c6768546..1f5df2c31 100644
--- a/test/regress/regress2/bv_to_int_ashr.smt2
+++ b/test/regress/regress2/bv_to_int_ashr.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_bitwise.smt2 b/test/regress/regress2/bv_to_int_bitwise.smt2
index 23624e12c..4dc37a94c 100644
--- a/test/regress/regress2/bv_to_int_bitwise.smt2
+++ b/test/regress/regress2/bv_to_int_bitwise.smt2
@@ -1,8 +1,10 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum
-; COMMAND-LINE: --solve-bv-as-int=bv
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=5 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))
diff --git a/test/regress/regress2/bv_to_int_bvmul1.smt2 b/test/regress/regress2/bv_to_int_bvmul1.smt2
index 232959f33..bf6f2cfc4 100644
--- a/test/regress/regress2/bv_to_int_bvmul1.smt2
+++ b/test/regress/regress2/bv_to_int_bvmul1.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
index babf9af32..2ecd0fe6c 100644
--- a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
+++ b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
@@ -1,4 +1,5 @@
-;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-unsat-cores
+;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+;COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
 ;EXPECT: unsat
 (set-logic QF_UFBV)
 (declare-fun z$n0s32 () (_ BitVec 32))
diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2
index 4b22c8ed8..28fb86f76 100644
--- a/test/regress/regress2/bv_to_int_inc1.smt2
+++ b/test/regress/regress2/bv_to_int_inc1.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --incremental --solve-bv-as-int=sum
+; COMMAND-LINE: --incremental --solve-bv-as-int=bitwise
 ; COMMAND-LINE: --incremental --solve-bv-as-int=iand
 ; COMMAND-LINE: --incremental --solve-bv-as-int=bv
 ; EXPECT sat
diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2
index 3b55c035d..c12138091 100644
--- a/test/regress/regress2/bv_to_int_mask_array_1.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores
 ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores
 ; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
 ; EXPECT: unsat
diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2
index edcc14149..17a113f85 100644
--- a/test/regress/regress2/bv_to_int_mask_array_2.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value
 ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum
 ; COMMAND-LINE: --solve-bv-as-int=bv
diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2
index 74e5ca95a..2b411209d 100644
--- a/test/regress/regress2/bv_to_int_mask_array_3.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4)))
diff --git a/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2
new file mode 100644
index 000000000..d454ad630
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
+; EXPECT: (error "Error in option parsing: --solve-bv-as-int=bitwise does not support quantifiers")
+; EXIT: 1
+(set-logic BV)
+(declare-const x (_ BitVec 8))
+(assert (forall ((y (_ BitVec 8)))
+               (distinct #b00000000
+                         (bvand x y))))
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
index bcc31c38c..173f1a552 100644
--- a/test/regress/regress2/bv_to_int_shifts.smt2
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))
diff --git a/test/regress/regress2/strings/strings-alpha-card-129.smt2 b/test/regress/regress2/strings/strings-alpha-card-129.smt2
deleted file mode 100644
index c0b4ae0a2..000000000
--- a/test/regress/regress2/strings/strings-alpha-card-129.smt2
+++ /dev/null
@@ -1,393 +0,0 @@
-; COMMAND-LINE: --strings-alpha-card=128 --simplification=none
-; EXPECT: unsat
-(set-logic QF_SLIA)
-(declare-fun s1 () String)
-(assert (= (str.len s1) 1))
-(declare-fun s2 () String)
-(assert (= (str.len s2) 1))
-(declare-fun s3 () String)
-(assert (= (str.len s3) 1))
-(declare-fun s4 () String)
-(assert (= (str.len s4) 1))
-(declare-fun s5 () String)
-(assert (= (str.len s5) 1))
-(declare-fun s6 () String)
-(assert (= (str.len s6) 1))
-(declare-fun s7 () String)
-(assert (= (str.len s7) 1))
-(declare-fun s8 () String)
-(assert (= (str.len s8) 1))
-(declare-fun s9 () String)
-(assert (= (str.len s9) 1))
-(declare-fun s10 () String)
-(assert (= (str.len s10) 1))
-(declare-fun s11 () String)
-(assert (= (str.len s11) 1))
-(declare-fun s12 () String)
-(assert (= (str.len s12) 1))
-(declare-fun s13 () String)
-(assert (= (str.len s13) 1))
-(declare-fun s14 () String)
-(assert (= (str.len s14) 1))
-(declare-fun s15 () String)
-(assert (= (str.len s15) 1))
-(declare-fun s16 () String)
-(assert (= (str.len s16) 1))
-(declare-fun s17 () String)
-(assert (= (str.len s17) 1))
-(declare-fun s18 () String)
-(assert (= (str.len s18) 1))
-(declare-fun s19 () String)
-(assert (= (str.len s19) 1))
-(declare-fun s20 () String)
-(assert (= (str.len s20) 1))
-(declare-fun s21 () String)
-(assert (= (str.len s21) 1))
-(declare-fun s22 () String)
-(assert (= (str.len s22) 1))
-(declare-fun s23 () String)
-(assert (= (str.len s23) 1))
-(declare-fun s24 () String)
-(assert (= (str.len s24) 1))
-(declare-fun s25 () String)
-(assert (= (str.len s25) 1))
-(declare-fun s26 () String)
-(assert (= (str.len s26) 1))
-(declare-fun s27 () String)
-(assert (= (str.len s27) 1))
-(declare-fun s28 () String)
-(assert (= (str.len s28) 1))
-(declare-fun s29 () String)
-(assert (= (str.len s29) 1))
-(declare-fun s30 () String)
-(assert (= (str.len s30) 1))
-(declare-fun s31 () String)
-(assert (= (str.len s31) 1))
-(declare-fun s32 () String)
-(assert (= (str.len s32) 1))
-(declare-fun s33 () String)
-(assert (= (str.len s33) 1))
-(declare-fun s34 () String)
-(assert (= (str.len s34) 1))
-(declare-fun s35 () String)
-(assert (= (str.len s35) 1))
-(declare-fun s36 () String)
-(assert (= (str.len s36) 1))
-(declare-fun s37 () String)
-(assert (= (str.len s37) 1))
-(declare-fun s38 () String)
-(assert (= (str.len s38) 1))
-(declare-fun s39 () String)
-(assert (= (str.len s39) 1))
-(declare-fun s40 () String)
-(assert (= (str.len s40) 1))
-(declare-fun s41 () String)
-(assert (= (str.len s41) 1))
-(declare-fun s42 () String)
-(assert (= (str.len s42) 1))
-(declare-fun s43 () String)
-(assert (= (str.len s43) 1))
-(declare-fun s44 () String)
-(assert (= (str.len s44) 1))
-(declare-fun s45 () String)
-(assert (= (str.len s45) 1))
-(declare-fun s46 () String)
-(assert (= (str.len s46) 1))
-(declare-fun s47 () String)
-(assert (= (str.len s47) 1))
-(declare-fun s48 () String)
-(assert (= (str.len s48) 1))
-(declare-fun s49 () String)
-(assert (= (str.len s49) 1))
-(declare-fun s50 () String)
-(assert (= (str.len s50) 1))
-(declare-fun s51 () String)
-(assert (= (str.len s51) 1))
-(declare-fun s52 () String)
-(assert (= (str.len s52) 1))
-(declare-fun s53 () String)
-(assert (= (str.len s53) 1))
-(declare-fun s54 () String)
-(assert (= (str.len s54) 1))
-(declare-fun s55 () String)
-(assert (= (str.len s55) 1))
-(declare-fun s56 () String)
-(assert (= (str.len s56) 1))
-(declare-fun s57 () String)
-(assert (= (str.len s57) 1))
-(declare-fun s58 () String)
-(assert (= (str.len s58) 1))
-(declare-fun s59 () String)
-(assert (= (str.len s59) 1))
-(declare-fun s60 () String)
-(assert (= (str.len s60) 1))
-(declare-fun s61 () String)
-(assert (= (str.len s61) 1))
-(declare-fun s62 () String)
-(assert (= (str.len s62) 1))
-(declare-fun s63 () String)
-(assert (= (str.len s63) 1))
-(declare-fun s64 () String)
-(assert (= (str.len s64) 1))
-(declare-fun s65 () String)
-(assert (= (str.len s65) 1))
-(declare-fun s66 () String)
-(assert (= (str.len s66) 1))
-(declare-fun s67 () String)
-(assert (= (str.len s67) 1))
-(declare-fun s68 () String)
-(assert (= (str.len s68) 1))
-(declare-fun s69 () String)
-(assert (= (str.len s69) 1))
-(declare-fun s70 () String)
-(assert (= (str.len s70) 1))
-(declare-fun s71 () String)
-(assert (= (str.len s71) 1))
-(declare-fun s72 () String)
-(assert (= (str.len s72) 1))
-(declare-fun s73 () String)
-(assert (= (str.len s73) 1))
-(declare-fun s74 () String)
-(assert (= (str.len s74) 1))
-(declare-fun s75 () String)
-(assert (= (str.len s75) 1))
-(declare-fun s76 () String)
-(assert (= (str.len s76) 1))
-(declare-fun s77 () String)
-(assert (= (str.len s77) 1))
-(declare-fun s78 () String)
-(assert (= (str.len s78) 1))
-(declare-fun s79 () String)
-(assert (= (str.len s79) 1))
-(declare-fun s80 () String)
-(assert (= (str.len s80) 1))
-(declare-fun s81 () String)
-(assert (= (str.len s81) 1))
-(declare-fun s82 () String)
-(assert (= (str.len s82) 1))
-(declare-fun s83 () String)
-(assert (= (str.len s83) 1))
-(declare-fun s84 () String)
-(assert (= (str.len s84) 1))
-(declare-fun s85 () String)
-(assert (= (str.len s85) 1))
-(declare-fun s86 () String)
-(assert (= (str.len s86) 1))
-(declare-fun s87 () String)
-(assert (= (str.len s87) 1))
-(declare-fun s88 () String)
-(assert (= (str.len s88) 1))
-(declare-fun s89 () String)
-(assert (= (str.len s89) 1))
-(declare-fun s90 () String)
-(assert (= (str.len s90) 1))
-(declare-fun s91 () String)
-(assert (= (str.len s91) 1))
-(declare-fun s92 () String)
-(assert (= (str.len s92) 1))
-(declare-fun s93 () String)
-(assert (= (str.len s93) 1))
-(declare-fun s94 () String)
-(assert (= (str.len s94) 1))
-(declare-fun s95 () String)
-(assert (= (str.len s95) 1))
-(declare-fun s96 () String)
-(assert (= (str.len s96) 1))
-(declare-fun s97 () String)
-(assert (= (str.len s97) 1))
-(declare-fun s98 () String)
-(assert (= (str.len s98) 1))
-(declare-fun s99 () String)
-(assert (= (str.len s99) 1))
-(declare-fun s100 () String)
-(assert (= (str.len s100) 1))
-(declare-fun s101 () String)
-(assert (= (str.len s101) 1))
-(declare-fun s102 () String)
-(assert (= (str.len s102) 1))
-(declare-fun s103 () String)
-(assert (= (str.len s103) 1))
-(declare-fun s104 () String)
-(assert (= (str.len s104) 1))
-(declare-fun s105 () String)
-(assert (= (str.len s105) 1))
-(declare-fun s106 () String)
-(assert (= (str.len s106) 1))
-(declare-fun s107 () String)
-(assert (= (str.len s107) 1))
-(declare-fun s108 () String)
-(assert (= (str.len s108) 1))
-(declare-fun s109 () String)
-(assert (= (str.len s109) 1))
-(declare-fun s110 () String)
-(assert (= (str.len s110) 1))
-(declare-fun s111 () String)
-(assert (= (str.len s111) 1))
-(declare-fun s112 () String)
-(assert (= (str.len s112) 1))
-(declare-fun s113 () String)
-(assert (= (str.len s113) 1))
-(declare-fun s114 () String)
-(assert (= (str.len s114) 1))
-(declare-fun s115 () String)
-(assert (= (str.len s115) 1))
-(declare-fun s116 () String)
-(assert (= (str.len s116) 1))
-(declare-fun s117 () String)
-(assert (= (str.len s117) 1))
-(declare-fun s118 () String)
-(assert (= (str.len s118) 1))
-(declare-fun s119 () String)
-(assert (= (str.len s119) 1))
-(declare-fun s120 () String)
-(assert (= (str.len s120) 1))
-(declare-fun s121 () String)
-(assert (= (str.len s121) 1))
-(declare-fun s122 () String)
-(assert (= (str.len s122) 1))
-(declare-fun s123 () String)
-(assert (= (str.len s123) 1))
-(declare-fun s124 () String)
-(assert (= (str.len s124) 1))
-(declare-fun s125 () String)
-(assert (= (str.len s125) 1))
-(declare-fun s126 () String)
-(assert (= (str.len s126) 1))
-(declare-fun s127 () String)
-(assert (= (str.len s127) 1))
-(declare-fun s128 () String)
-(assert (= (str.len s128) 1))
-(declare-fun s129 () String)
-(assert (= (str.len s129) 1))
-(assert (distinct
-s1
-s2
-s3
-s4
-s5
-s6
-s7
-s8
-s9
-s10
-s11
-s12
-s13
-s14
-s15
-s16
-s17
-s18
-s19
-s20
-s21
-s22
-s23
-s24
-s25
-s26
-s27
-s28
-s29
-s30
-s31
-s32
-s33
-s34
-s35
-s36
-s37
-s38
-s39
-s40
-s41
-s42
-s43
-s44
-s45
-s46
-s47
-s48
-s49
-s50
-s51
-s52
-s53
-s54
-s55
-s56
-s57
-s58
-s59
-s60
-s61
-s62
-s63
-s64
-s65
-s66
-s67
-s68
-s69
-s70
-s71
-s72
-s73
-s74
-s75
-s76
-s77
-s78
-s79
-s80
-s81
-s82
-s83
-s84
-s85
-s86
-s87
-s88
-s89
-s90
-s91
-s92
-s93
-s94
-s95
-s96
-s97
-s98
-s99
-s100
-s101
-s102
-s103
-s104
-s105
-s106
-s107
-s108
-s109
-s110
-s111
-s112
-s113
-s114
-s115
-s116
-s117
-s118
-s119
-s120
-s121
-s122
-s123
-s124
-s125
-s126
-s127
-s128
-s129
-))
-(check-sat)
diff --git a/test/regress/regress2/strings/strings-alpha-card-65.smt2 b/test/regress/regress2/strings/strings-alpha-card-65.smt2
new file mode 100644
index 000000000..82ab06ea9
--- /dev/null
+++ b/test/regress/regress2/strings/strings-alpha-card-65.smt2
@@ -0,0 +1,201 @@
+; COMMAND-LINE: --strings-alpha-card=64 --simplification=none
+; EXPECT: unsat
+(set-logic QF_SLIA)
+(declare-fun s1 () String)
+(assert (= (str.len s1) 1))
+(declare-fun s2 () String)
+(assert (= (str.len s2) 1))
+(declare-fun s3 () String)
+(assert (= (str.len s3) 1))
+(declare-fun s4 () String)
+(assert (= (str.len s4) 1))
+(declare-fun s5 () String)
+(assert (= (str.len s5) 1))
+(declare-fun s6 () String)
+(assert (= (str.len s6) 1))
+(declare-fun s7 () String)
+(assert (= (str.len s7) 1))
+(declare-fun s8 () String)
+(assert (= (str.len s8) 1))
+(declare-fun s9 () String)
+(assert (= (str.len s9) 1))
+(declare-fun s10 () String)
+(assert (= (str.len s10) 1))
+(declare-fun s11 () String)
+(assert (= (str.len s11) 1))
+(declare-fun s12 () String)
+(assert (= (str.len s12) 1))
+(declare-fun s13 () String)
+(assert (= (str.len s13) 1))
+(declare-fun s14 () String)
+(assert (= (str.len s14) 1))
+(declare-fun s15 () String)
+(assert (= (str.len s15) 1))
+(declare-fun s16 () String)
+(assert (= (str.len s16) 1))
+(declare-fun s17 () String)
+(assert (= (str.len s17) 1))
+(declare-fun s18 () String)
+(assert (= (str.len s18) 1))
+(declare-fun s19 () String)
+(assert (= (str.len s19) 1))
+(declare-fun s20 () String)
+(assert (= (str.len s20) 1))
+(declare-fun s21 () String)
+(assert (= (str.len s21) 1))
+(declare-fun s22 () String)
+(assert (= (str.len s22) 1))
+(declare-fun s23 () String)
+(assert (= (str.len s23) 1))
+(declare-fun s24 () String)
+(assert (= (str.len s24) 1))
+(declare-fun s25 () String)
+(assert (= (str.len s25) 1))
+(declare-fun s26 () String)
+(assert (= (str.len s26) 1))
+(declare-fun s27 () String)
+(assert (= (str.len s27) 1))
+(declare-fun s28 () String)
+(assert (= (str.len s28) 1))
+(declare-fun s29 () String)
+(assert (= (str.len s29) 1))
+(declare-fun s30 () String)
+(assert (= (str.len s30) 1))
+(declare-fun s31 () String)
+(assert (= (str.len s31) 1))
+(declare-fun s32 () String)
+(assert (= (str.len s32) 1))
+(declare-fun s33 () String)
+(assert (= (str.len s33) 1))
+(declare-fun s34 () String)
+(assert (= (str.len s34) 1))
+(declare-fun s35 () String)
+(assert (= (str.len s35) 1))
+(declare-fun s36 () String)
+(assert (= (str.len s36) 1))
+(declare-fun s37 () String)
+(assert (= (str.len s37) 1))
+(declare-fun s38 () String)
+(assert (= (str.len s38) 1))
+(declare-fun s39 () String)
+(assert (= (str.len s39) 1))
+(declare-fun s40 () String)
+(assert (= (str.len s40) 1))
+(declare-fun s41 () String)
+(assert (= (str.len s41) 1))
+(declare-fun s42 () String)
+(assert (= (str.len s42) 1))
+(declare-fun s43 () String)
+(assert (= (str.len s43) 1))
+(declare-fun s44 () String)
+(assert (= (str.len s44) 1))
+(declare-fun s45 () String)
+(assert (= (str.len s45) 1))
+(declare-fun s46 () String)
+(assert (= (str.len s46) 1))
+(declare-fun s47 () String)
+(assert (= (str.len s47) 1))
+(declare-fun s48 () String)
+(assert (= (str.len s48) 1))
+(declare-fun s49 () String)
+(assert (= (str.len s49) 1))
+(declare-fun s50 () String)
+(assert (= (str.len s50) 1))
+(declare-fun s51 () String)
+(assert (= (str.len s51) 1))
+(declare-fun s52 () String)
+(assert (= (str.len s52) 1))
+(declare-fun s53 () String)
+(assert (= (str.len s53) 1))
+(declare-fun s54 () String)
+(assert (= (str.len s54) 1))
+(declare-fun s55 () String)
+(assert (= (str.len s55) 1))
+(declare-fun s56 () String)
+(assert (= (str.len s56) 1))
+(declare-fun s57 () String)
+(assert (= (str.len s57) 1))
+(declare-fun s58 () String)
+(assert (= (str.len s58) 1))
+(declare-fun s59 () String)
+(assert (= (str.len s59) 1))
+(declare-fun s60 () String)
+(assert (= (str.len s60) 1))
+(declare-fun s61 () String)
+(assert (= (str.len s61) 1))
+(declare-fun s62 () String)
+(assert (= (str.len s62) 1))
+(declare-fun s63 () String)
+(assert (= (str.len s63) 1))
+(declare-fun s64 () String)
+(assert (= (str.len s64) 1))
+(declare-fun s65 () String)
+(assert (= (str.len s65) 1))
+(assert (distinct
+s1
+s2
+s3
+s4
+s5
+s6
+s7
+s8
+s9
+s10
+s11
+s12
+s13
+s14
+s15
+s16
+s17
+s18
+s19
+s20
+s21
+s22
+s23
+s24
+s25
+s26
+s27
+s28
+s29
+s30
+s31
+s32
+s33
+s34
+s35
+s36
+s37
+s38
+s39
+s40
+s41
+s42
+s43
+s44
+s45
+s46
+s47
+s48
+s49
+s50
+s51
+s52
+s53
+s54
+s55
+s56
+s57
+s58
+s59
+s60
+s61
+s62
+s63
+s64
+s65
+))
+(check-sat)
diff --git a/test/regress/regress2/sygus/multi-udiv.sy b/test/regress/regress2/sygus/multi-udiv.sy
index d9deb28a3..65e5d428f 100644
--- a/test/regress/regress2/sygus/multi-udiv.sy
+++ b/test/regress/regress2/sygus/multi-udiv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum
 (set-logic BV)
 
 (define-fun hd05 ((x (_ BitVec 32))) (_ BitVec 32) (bvor x (bvsub x #x00000001)))
diff --git a/test/regress/regress2/sygus/sets-fun-test.sy b/test/regress/regress2/sygus/sets-fun-test.sy
index 43a8b36a9..23abc5c7e 100644
--- a/test/regress/regress2/sygus/sets-fun-test.sy
+++ b/test/regress/regress2/sygus/sets-fun-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum
 (set-logic ALL)
 (synth-fun f ((x Int)) (Set Int))
 
diff --git a/test/regress/regress2/sygus/three.sy b/test/regress/regress2/sygus/three.sy
index 239f7f498..9bed1e667 100644
--- a/test/regress/regress2/sygus/three.sy
+++ b/test/regress/regress2/sygus/three.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum
 
 (set-logic NIA)