The decision procedure options which are used for the UCLID 1.0 distribution 
are present in the <uclid-dir>/bin/uclid file. If you look at the file it will look like:

       camlrunm uclid_bc  <uclid-dir>/uclid_1_0_bc /usr/local/bin/perl  $* 1 1 bgv 0 0 0

The option after $* specifies the encoding method in UCLID. Currently it is 1 (as shown above).

The different options can be set as follows:

   1. SD (CAV02 Bryant-Lahiri-Seshia) : Option = 1 (default)
               - Uses small domain throughout

   2. EIJ (CAV02 Strichman-Seshia-Bryant) : Option = 6
               - Uses EIJ Method throughout

   3. Hybrid1 (CFV02 Bryant-Lahiri-Seshia) : Option = 4
              - This option is briefly mentioned in the CFV workshop paper.  Uses SD + 
                (EIJ method from Bryant-Velev CAV00). Uses EIJ for only those "variable classes" 
                (see CAV02 paper) which only supports equality between variables (e.g. x=y). 

   4. Hybrid2 (DAC03 Seshia-Lahiri-Bryant) : Option = 8
              - Also requires you to change the last option (the last of 0 0 0 in the uclid file), 
                currently 0, to a number that specifies a "threshold" value (see DAC03 paper). 
                We advise setting it somewhere in the range 50-500, but this value is platform-
                dependent, and the best value for you might be different (the paper uses an 
                automatic technique to set this, but it is not integrated into UCLID 1.0).


   There are other settings, but these 4 are the most useful ones.