Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

README

@@ -41,3 +41,5 @@ Remark: clang does not support OpenMP yet.
    cd build
    make
 
+
+To clean Z3 you can delete the build directory and run the mk_make.py script again.

src/api/java/AST.java

@@ -28,7 +28,8 @@ public class AST extends Z3Object
 
     /**
      * Object comparison.
-     * <param name="o">another AST</param>
+     * 
+	 * @param o another AST
      **/    
     public boolean equals(Object o)
     {
@@ -46,10 +47,12 @@ public class AST extends Z3Object
     }
 
     /**
-     * Object Comparison. <param name="other">Another AST</param>
+     * Object Comparison. 
+	 * @param other Another AST
      * 
-     * @return Negative if the object should be sorted before <paramref
+     * @return Negative if the object should be sorted before {@code other}, 
-     *         name="other"/>, positive if after else zero.
+     * positive if after else zero.
+     * @throws Z3Exception on error
      **/
     public int compareTo(Object other) throws Z3Exception
     {
@@ -90,6 +93,7 @@ public class AST extends Z3Object
 
     /**
      * A unique identifier for the AST (unique among all ASTs).
+     * @throws Z3Exception on error
      **/
     public int getId() throws Z3Exception
     {
@@ -97,10 +101,11 @@ public class AST extends Z3Object
     }
 
     /**
-     * Translates (copies) the AST to the Context <paramref name="ctx"/>. <param
+     * Translates (copies) the AST to the Context {@code ctx}. 
-     * name="ctx">A context</param>
+	 * @param ctx A context
      * 
-     * @return A copy of the AST which is associated with <paramref name="ctx"/>
+     * @return A copy of the AST which is associated with {@code ctx}
+     * @throws Z3Exception on error
      **/
     public AST translate(Context ctx) throws Z3Exception
     {
@@ -114,6 +119,7 @@ public class AST extends Z3Object
 
     /**
      * The kind of the AST.
+     * @throws Z3Exception on error
      **/
     public Z3_ast_kind getASTKind() throws Z3Exception
     {
@@ -123,6 +129,8 @@ public class AST extends Z3Object
 
     /**
      * Indicates whether the AST is an Expr
+     * @throws Z3Exception on error
+	 * @throws Z3Exception on error
      **/
     public boolean isExpr() throws Z3Exception
     {
@@ -140,6 +148,8 @@ public class AST extends Z3Object
 
     /**
      * Indicates whether the AST is an application
+	 * @return a boolean
+     * @throws Z3Exception on error
      **/
     public boolean isApp() throws Z3Exception
     {
@@ -147,7 +157,9 @@ public class AST extends Z3Object
     }
 
     /**
-     * Indicates whether the AST is a BoundVariable
+     * Indicates whether the AST is a BoundVariable.
+	 * @return a boolean
+     * @throws Z3Exception on error
      **/
     public boolean isVar() throws Z3Exception
     {
@@ -156,6 +168,8 @@ public class AST extends Z3Object
 
     /**
      * Indicates whether the AST is a Quantifier
+	 * @return a boolean
+     * @throws Z3Exception on error
      **/
     public boolean isQuantifier() throws Z3Exception
     {

src/api/java/ASTMap.java

@@ -23,10 +23,10 @@ package com.microsoft.z3;
 class ASTMap extends Z3Object
 {
     /**
-     * Checks whether the map contains the key <paramref name="k"/>. <param
+     * Checks whether the map contains the key {@code k}. 
-     * name="k">An AST</param>
+	 * @param k An AST
      * 
-     * @return True if <paramref name="k"/> is a key in the map, false
+     * @return True if {@code k} is a key in the map, false
      *         otherwise.
      **/
     public boolean contains(AST k) throws Z3Exception
@@ -37,9 +37,10 @@ class ASTMap extends Z3Object
     }
 
     /**
-     * Finds the value associated with the key <paramref name="k"/>. <remarks>
+     * Finds the value associated with the key {@code k}. 
-     * This function signs an error when <paramref name="k"/> is not a key in
+     * Remarks: This function signs an error when {@code k} is not a key in
-     * the map. </remarks> <param name="k">An AST</param>
+     * the map. 
+	 * @param k An AST
      * 
      * @throws Z3Exception
      **/
@@ -50,8 +51,9 @@ class ASTMap extends Z3Object
     }
 
     /**
-     * Stores or replaces a new key/value pair in the map. <param name="k">The
+     * Stores or replaces a new key/value pair in the map. 
-     * key AST</param> <param name="v">The value AST</param>
+	 * @param k The key AST
+	 * @param v The value AST
      **/
     public void insert(AST k, AST v) throws Z3Exception
     {
@@ -61,12 +63,11 @@ class ASTMap extends Z3Object
     }
 
     /**
-     * Erases the key <paramref name="k"/> from the map. <param name="k">An
+     * Erases the key {@code k} from the map. 
-     * AST</param>
+	 * @param k An AST
      **/
     public void erase(AST k) throws Z3Exception
     {
-
         Native.astMapErase(getContext().nCtx(), getNativeObject(), k.getNativeObject());
     }
 

src/api/java/ASTVector.java

@@ -31,9 +31,10 @@ class ASTVector extends Z3Object
     }
 
     /**
-     * Retrieves the i-th object in the vector. <remarks>May throw an
+     * Retrieves the i-th object in the vector.
-     * IndexOutOfBoundsException when <paramref name="i"/> is out of
+     * Remarks: May throw an {@code IndexOutOfBoundsException} when 
-     * range.</remarks> <param name="i">Index</param>
+     * {@code i} is out of range. 
+	 * @param i Index
      * 
      * @return An AST
      * @throws Z3Exception
@@ -52,8 +53,8 @@ class ASTVector extends Z3Object
     }
 
     /**
-     * Resize the vector to <paramref name="newSize"/>. <param
+     * Resize the vector to {@code newSize}. 
-     * name="newSize">The new size of the vector.</param>
+	 * @param newSize The new size of the vector.
      **/
     public void resize(int newSize) throws Z3Exception
     {
@@ -61,8 +62,9 @@ class ASTVector extends Z3Object
     }
 
     /**
-     * Add the AST <paramref name="a"/> to the back of the vector. The size is
+     * Add the AST {@code a} to the back of the vector. The size is
-     * increased by 1. <param name="a">An AST</param>
+     * increased by 1. 
+	 * @param a An AST
      **/
     public void push(AST a) throws Z3Exception
     {
@@ -70,8 +72,8 @@ class ASTVector extends Z3Object
     }
 
     /**
-     * Translates all ASTs in the vector to <paramref name="ctx"/>. <param
+     * Translates all ASTs in the vector to {@code ctx}. 
-     * name="ctx">A context</param>
+	 * @param ctx A context
      * 
      * @return A new ASTVector
      * @throws Z3Exception

src/api/java/AlgebraicNum.java

@@ -24,11 +24,13 @@ public class AlgebraicNum extends ArithExpr
 {
 	/**
 	 * Return a upper bound for a given real algebraic number. The interval
-	 * isolating the number is smaller than 1/10^<paramref name="precision"/>.
+	 * isolating the number is smaller than 1/10^{@code precision}.
-	 * <seealso cref="Expr.IsAlgebraicNumber"/> <param name="precision">the
+	 * 
-	 * precision of the result</param>
+	 * @see Expr#isAlgebraicNumber
+	 * @param precision the precision of the result
 	 * 
 	 * @return A numeral Expr of sort Real
+	 * @throws Z3Exception on error
 	 **/
 	public RatNum toUpper(int precision) throws Z3Exception
 	{
@@ -39,10 +41,13 @@ public class AlgebraicNum extends ArithExpr
 
 	/**
 	 * Return a lower bound for the given real algebraic number. The interval
-	 * isolating the number is smaller than 1/10^<paramref name="precision"/>.
+	 * isolating the number is smaller than 1/10^{@code precision}.
-	 * <seealso cref="Expr.IsAlgebraicNumber"/> <param name="precision"></param>
+	 * 
+	 * @see Expr#isAlgebraicNumber
+	 * @param precision precision
 	 * 
 	 * @return A numeral Expr of sort Real
+	 * @throws Z3Exception on error
 	 **/
 	public RatNum toLower(int precision) throws Z3Exception
 	{
@@ -52,8 +57,11 @@ public class AlgebraicNum extends ArithExpr
 	}
 
 	/**
-	 * Returns a string representation in decimal notation. <remarks>The result
+	 * Returns a string representation in decimal notation.
-	 * has at most <paramref name="precision"/> decimal places.</remarks>
+	 * Remarks: The result has at most {@code precision} decimal places.
+	 * @param precision precision
+	 * @return String
+	 * @throws Z3Exception on error
 	 **/
 	public String toDecimal(int precision) throws Z3Exception
 	{

src/api/java/ApplyResult.java

@@ -48,10 +48,10 @@ public class ApplyResult extends Z3Object
     }
 
     /**
-     * Convert a model for the subgoal <paramref name="i"/> into a model for the
+     * Convert a model for the subgoal {@code i} into a model for the
-     * original goal <code>g</code>, that the ApplyResult was obtained from.
+     * original goal {@code g}, that the ApplyResult was obtained from.
      * 
-     * @return A model for <code>g</code>
+     * @return A model for {@code g}
      * @throws Z3Exception
      **/
     public Model convertModel(int i, Model m) throws Z3Exception

src/api/java/ArithExpr.java

@@ -23,7 +23,7 @@ package com.microsoft.z3;
 public class ArithExpr extends Expr
 {
 	/**
-	 * Constructor for ArithExpr </summary>
+	 * Constructor for ArithExpr
 	 **/
 	protected ArithExpr(Context ctx)
 	{

src/api/java/ArrayExpr.java

@@ -24,7 +24,7 @@ package com.microsoft.z3;
 public class ArrayExpr extends Expr
 {
 	/**
-	 * Constructor for ArrayExpr </summary>
+	 * Constructor for ArrayExpr
 	 **/
 	protected ArrayExpr(Context ctx)
 	{

src/api/java/ArraySort.java

@@ -25,6 +25,8 @@ public class ArraySort extends Sort
 	/**
 	 * The domain of the array sort.
 	 * @throws Z3Exception 
+	 * @throws Z3Exception on error
+	 * @return a sort
 	 **/
 	public Sort getDomain() throws Z3Exception
 	{
@@ -35,6 +37,8 @@ public class ArraySort extends Sort
 	/**
 	 * The range of the array sort.
 	 * @throws Z3Exception 
+	 * @throws Z3Exception on error
+	 * @return a sort
 	 **/
 	public Sort getRange() throws Z3Exception
 	{

src/api/java/BitVecExpr.java

@@ -26,6 +26,8 @@ public class BitVecExpr extends Expr
 	/**
 	 * The size of the sort of a bit-vector term.
 	 * @throws Z3Exception 
+	 * @throws Z3Exception on error
+	 * @return an int
 	 **/
 	public int getSortSize() throws Z3Exception
 	{
@@ -33,7 +35,7 @@ public class BitVecExpr extends Expr
 	}
 
 	/**
-	 * Constructor for BitVecExpr </summary>
+	 * Constructor for BitVecExpr
 	 **/
 	BitVecExpr(Context ctx)
 	{

src/api/java/BitVecSort.java

@@ -24,6 +24,8 @@ public class BitVecSort extends Sort
 {
 	/**
 	 * The size of the bit-vector sort.
+	 * @throws Z3Exception on error
+	 * @return an int
 	 **/
 	public int getSize() throws Z3Exception
 	{

src/api/java/BoolExpr.java

@@ -23,7 +23,7 @@ package com.microsoft.z3;
 public class BoolExpr extends Expr
 {
 	/**
-	 * Constructor for BoolExpr </summary>
+	 * Constructor for BoolExpr
 	 **/
 	protected BoolExpr(Context ctx)
 	{
@@ -31,8 +31,9 @@ public class BoolExpr extends Expr
 	}
 
 	/**
-	 * Constructor for BoolExpr </summary>
+	 * Constructor for BoolExpr
 	 * @throws Z3Exception 
+	 * @throws Z3Exception on error
 	 **/
 	BoolExpr(Context ctx, long obj) throws Z3Exception
 	{

src/api/java/Constructor.java

@@ -25,6 +25,8 @@ public class Constructor extends Z3Object
 	/**
 	 * The number of fields of the constructor.
 	 * @throws Z3Exception 
+	 * @throws Z3Exception on error
+	 * @return an int
 	 **/
 	public int getNumFields() throws Z3Exception
 	{	
@@ -34,6 +36,7 @@ public class Constructor extends Z3Object
 	/**
 	 * The function declaration of the constructor.
 	 * @throws Z3Exception 
+	 * @throws Z3Exception on error
 	 **/
 	public FuncDecl ConstructorDecl() throws Z3Exception
 	{
@@ -47,6 +50,7 @@ public class Constructor extends Z3Object
 	/**
 	 * The function declaration of the tester.
 	 * @throws Z3Exception 
+	 * @throws Z3Exception on error
 	 **/
 	public FuncDecl getTesterDecl() throws Z3Exception
 	{
@@ -60,6 +64,7 @@ public class Constructor extends Z3Object
 	/**
 	 * The function declarations of the accessors
 	 * @throws Z3Exception 
+	 * @throws Z3Exception on error
 	 **/
 	public FuncDecl[] getAccessorDecls() throws Z3Exception
 	{
@@ -75,6 +80,7 @@ public class Constructor extends Z3Object
 
 	/**
 	 * Destructor.
+	 * @throws Z3Exception on error
 	 **/
 	protected void finalize() throws Z3Exception
 	{

src/api/java/ConstructorList.java

@@ -24,6 +24,7 @@ public class ConstructorList extends Z3Object
 {
 	/**
 	 * Destructor.
+	 * @throws Z3Exception on error
 	 **/
 	protected void finalize() throws Z3Exception
 	{

src/api/java/DatatypeExpr.java

@@ -23,7 +23,7 @@ package com.microsoft.z3;
 public class DatatypeExpr extends Expr
 {
 	/**
-	 * Constructor for DatatypeExpr </summary>
+	 * Constructor for DatatypeExpr
 	 **/
 	protected DatatypeExpr(Context ctx)
 	{

src/api/java/DatatypeSort.java

@@ -24,6 +24,8 @@ public class DatatypeSort extends Sort
 {
 	/**
 	 * The number of constructors of the datatype sort.
+	 * @throws Z3Exception on error
+	 * @return an int
 	 **/
 	public int getNumConstructors() throws Z3Exception
 	{
@@ -35,6 +37,7 @@ public class DatatypeSort extends Sort
 	 * The constructors.
 	 * 
 	 * @throws Z3Exception
+	 * @throws Z3Exception on error
 	 **/
 	public FuncDecl[] getConstructors() throws Z3Exception
 	{
@@ -50,6 +53,7 @@ public class DatatypeSort extends Sort
 	 * The recognizers.
 	 * 
 	 * @throws Z3Exception
+	 * @throws Z3Exception on error
 	 **/
 	public FuncDecl[] getRecognizers() throws Z3Exception
 	{
@@ -65,6 +69,7 @@ public class DatatypeSort extends Sort
 	 * The constructor accessors.
 	 * 
 	 * @throws Z3Exception
+	 * @throws Z3Exception on error
 	 **/
 	public FuncDecl[][] getAccessors() throws Z3Exception
 	{

src/api/java/EnumSort.java

@@ -24,6 +24,7 @@ public class EnumSort extends Sort
 {
 	/**
 	 * The function declarations of the constants in the enumeration.
+	 * @throws Z3Exception on error
 	 **/
 	public FuncDecl[] getConstDecls() throws Z3Exception
 	{
@@ -36,6 +37,8 @@ public class EnumSort extends Sort
 
 	/**
 	 * The constants in the enumeration.
+	 * @throws Z3Exception on error
+	 * @return an Expr
 	 **/
 	public Expr[] getConsts() throws Z3Exception
 	{	    
@@ -48,6 +51,7 @@ public class EnumSort extends Sort
 
 	/**
 	 * The test predicates for the constants in the enumeration.
+	 * @throws Z3Exception on error
 	 **/
 	public FuncDecl[] getTesterDecls() throws Z3Exception
 	{

src/api/java/FiniteDomainSort.java

@@ -24,6 +24,7 @@ public class FiniteDomainSort extends Sort
 {
 	/**
 	 * The size of the finite domain sort.
+	 * @throws Z3Exception on error
 	 **/
 	public long getSize() throws Z3Exception
 	{

src/api/java/Fixedpoint.java

@@ -163,7 +163,8 @@ public class Fixedpoint extends Z3Object
     }
 
     /**
-     * Creates a backtracking point. <seealso cref="Pop"/>
+     * Creates a backtracking point. 
+	 * @see pop
      **/
     public void push() throws Z3Exception
     {
@@ -171,9 +172,11 @@ public class Fixedpoint extends Z3Object
     }
 
     /**
-     * Backtrack one backtracking point. <remarks>Note that an exception is
+     * Backtrack one backtracking point.
-     * thrown if Pop is called without a corresponding <code>Push</code>
+	 * Remarks: Note that an exception is thrown if {#code pop} 
-     * </remarks> <seealso cref="Push"/>
+	 * is called without a corresponding {@code push}
+     *  
+	 * @see push
      **/
     public void pop() throws Z3Exception
     {

src/api/java/FuncDecl.java

@@ -29,7 +29,7 @@ public class FuncDecl extends AST
     /**
      * Comparison operator.
      * 
-     * @return True if <paramref name="a"/> and <paramref name="b"/> share the
+     * @return True if {@code a"/> and <paramref name="b} share the
      *         same context and are equal, false otherwise.
      **/
     /* Overloaded operators are not translated. */
@@ -37,7 +37,7 @@ public class FuncDecl extends AST
     /**
      * Comparison operator.
      * 
-     * @return True if <paramref name="a"/> and <paramref name="b"/> do not
+     * @return True if {@code a"/> and <paramref name="b} do not
      *         share the same context or are not equal, false otherwise.
      **/
     /* Overloaded operators are not translated. */
@@ -92,8 +92,8 @@ public class FuncDecl extends AST
     }
 
     /**
-     * The size of the domain of the function declaration <seealso
+     * The size of the domain of the function declaration 
-     * cref="Arity"/>
+	 * @see getArity
      **/
     public int getDomainSize() throws Z3Exception
     {
@@ -221,7 +221,7 @@ public class FuncDecl extends AST
         private String r;
 
         /**
-         * The int value of the parameter.</summary>
+         * The int value of the parameter.
          **/
         public int getInt() throws Z3Exception
         {
@@ -231,7 +231,7 @@ public class FuncDecl extends AST
         }
 
         /**
-         * The double value of the parameter.</summary>
+         * The double value of the parameter.
          **/
         public double getDouble() throws Z3Exception
         {
@@ -241,7 +241,7 @@ public class FuncDecl extends AST
         }
 
         /**
-         * The Symbol value of the parameter.</summary>
+         * The Symbol value of the parameter.
          **/
         public Symbol getSymbol() throws Z3Exception
         {
@@ -251,7 +251,7 @@ public class FuncDecl extends AST
         }
 
         /**
-         * The Sort value of the parameter.</summary>
+         * The Sort value of the parameter.
          **/
         public Sort getSort() throws Z3Exception
         {
@@ -261,7 +261,7 @@ public class FuncDecl extends AST
         }
 
         /**
-         * The AST value of the parameter.</summary>
+         * The AST value of the parameter.
          **/
         public AST getAST() throws Z3Exception
         {
@@ -271,7 +271,7 @@ public class FuncDecl extends AST
         }
 
         /**
-         * The FunctionDeclaration value of the parameter.</summary>
+         * The FunctionDeclaration value of the parameter.
          **/
         public FuncDecl getFuncDecl() throws Z3Exception
         {
@@ -281,7 +281,7 @@ public class FuncDecl extends AST
         }
 
         /**
-         * The rational string value of the parameter.</summary>
+         * The rational string value of the parameter.
          **/
         public String getRational() throws Z3Exception
         {
@@ -375,8 +375,8 @@ public class FuncDecl extends AST
     }
 
     /**
-     * Create expression that applies function to arguments. <param
+     * Create expression that applies function to arguments. 
-     * name="args"></param>
+	 * @param args 
      * 
      * @return
      **/

src/api/java/FuncInterp.java

@@ -34,7 +34,8 @@ public class FuncInterp extends Z3Object
 		 * Return the (symbolic) value of this entry.
 		 * 
 		 * @throws Z3Exception
-		 **/
+		 * @throws Z3Exception on error
+	 **/
 		public Expr getValue() throws Z3Exception
 		{
 			return Expr.create(getContext(),
@@ -43,7 +44,8 @@ public class FuncInterp extends Z3Object
 
 		/**
 		 * The number of arguments of the entry.
-		 **/
+		 * @throws Z3Exception on error
+	 **/
 		public int getNumArgs() throws Z3Exception
 		{
 			return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
@@ -53,7 +55,8 @@ public class FuncInterp extends Z3Object
 		 * The arguments of the function entry.
 		 * 
 		 * @throws Z3Exception
-		 **/
+		 * @throws Z3Exception on error
+	 **/
 		public Expr[] getArgs() throws Z3Exception
 		{
 			int n = getNumArgs();
@@ -103,6 +106,8 @@ public class FuncInterp extends Z3Object
 
 	/**
 	 * The number of entries in the function interpretation.
+	 * @throws Z3Exception on error
+	 * @return an int
 	 **/
 	public int getNumEntries() throws Z3Exception
 	{
@@ -113,6 +118,7 @@ public class FuncInterp extends Z3Object
 	 * The entries in the function interpretation
 	 * 
 	 * @throws Z3Exception
+	 * @throws Z3Exception on error
 	 **/
 	public Entry[] getEntries() throws Z3Exception
 	{
@@ -128,6 +134,8 @@ public class FuncInterp extends Z3Object
 	 * The (symbolic) `else' value of the function interpretation.
 	 * 
 	 * @throws Z3Exception
+	 * @throws Z3Exception on error
+	 * @return an Expr
 	 **/
 	public Expr getElse() throws Z3Exception
 	{
@@ -137,6 +145,8 @@ public class FuncInterp extends Z3Object
 
 	/**
 	 * The arity of the function interpretation
+	 * @throws Z3Exception on error
+	 * @return an int
 	 **/
 	public int getArity() throws Z3Exception
 	{

src/api/java/Global.java

@@ -19,16 +19,16 @@ package com.microsoft.z3;
 
 /**
  * Global functions for Z3. 
- * <remarks>
+ * Remarks: 
  * This (static) class contains functions that effect the behaviour of Z3
  * globally across contexts, etc. 
- * </remarks>
+ * 
  **/
 public final class Global
 {
     /**
      * Set a global (or module) parameter, which is shared by all Z3 contexts.
-     * <remarks>
+     * Remarks: 
      * When a Z3 module is initialized it will use the value of these parameters
      * when Z3_params objects are not provided.
      * The name of parameter can be composed of characters [a-z][A-Z], digits [0-9], '-' and '_'. 
@@ -36,11 +36,11 @@ public final class Global
      * The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'.
      * Thus, the following parameter names are considered equivalent: "pp.decimal-precision"  and "PP.DECIMAL_PRECISION".
      * This function can be used to set parameters for a specific Z3 module.
-     * This can be done by using <module-name>.<parameter-name>.
+     * This can be done by using &lt;module-name&gt;.&lt;parameter-name&gt;.
      * For example:
      * Z3_global_param_set('pp.decimal', 'true')
      * will set the parameter "decimal" in the module "pp" to true.
-     * </remarks>
+     * 
      **/
     public static void setParameter(String id, String value)
     {
@@ -49,11 +49,10 @@ public final class Global
     
     /**
      * Get a global (or module) parameter.     
-     * <remarks>               
+     * Remarks:     
-     * Returns null if the parameter <param name="id">parameter id</param> does not exist.     
      * This function cannot be invoked simultaneously from different threads without synchronization.
      * The result string stored in param_value is stored in a shared location.
-     * </remarks>
+     * @return null if the parameter {@code id} does not exist.
      **/
     public static String getParameter(String id)
     {
@@ -66,10 +65,9 @@ public final class Global
     
     /**
      * Restore the value of all global (and module) parameters.
-     * <remarks>
+     * Remarks: 
      * This command will not affect already created objects (such as tactics and solvers)
-     * </remarks>
+	 * @see setParameter
-     * <seealso cref="SetParameter"/>
      **/
     public static void resetParameters()
     {

src/api/java/Goal.java

@@ -26,11 +26,12 @@ import com.microsoft.z3.enumerations.Z3_goal_prec;
 public class Goal extends Z3Object
 {
     /**
-     * The precision of the goal. <remarks> Goals can be transformed using over
+     * The precision of the goal.
+	 * Remarks:  Goals can be transformed using over
      * and under approximations. An under approximation is applied when the
      * objective is to find a model for a given goal. An over approximation is
      * applied when the objective is to find a proof for a given goal.
-     * </remarks>
+     * 
      **/
     public Z3_goal_prec getPrecision() throws Z3Exception
     {
@@ -72,7 +73,7 @@ public class Goal extends Z3Object
     }
 
     /**
-     * Adds the <paramref name="constraints"/> to the given goal.
+     * Adds the {@code constraints} to the given goal.
      * 
      * @throws Z3Exception
      **/
@@ -95,8 +96,9 @@ public class Goal extends Z3Object
     }
 
     /**
-     * The depth of the goal. <remarks> This tracks how many transformations
+     * The depth of the goal.
-     * were applied to it. </remarks>
+	 * Remarks:  This tracks how many transformations
+     * were applied to it. 
      **/
     public int getDepth() throws Z3Exception
     {
@@ -162,8 +164,7 @@ public class Goal extends Z3Object
     }
 
     /**
-     * Translates (copies) the Goal to the target Context <paramref
+     * Translates (copies) the Goal to the target Context {@code ctx}.
-     * name="ctx"/>.
      * 
      * @throws Z3Exception
      **/
@@ -174,8 +175,9 @@ public class Goal extends Z3Object
     }
 
     /**
-     * Simplifies the goal. <remarks>Essentially invokes the `simplify' tactic
+     * Simplifies the goal.
-     * on the goal.</remarks>
+	 * Remarks: Essentially invokes the `simplify' tactic
+     * on the goal.
      **/
     public Goal simplify() throws Z3Exception
     {
@@ -189,8 +191,9 @@ public class Goal extends Z3Object
     }
     
     /**
-     * Simplifies the goal. <remarks>Essentially invokes the `simplify' tactic
+     * Simplifies the goal.
-     * on the goal.</remarks>
+	 * Remarks: Essentially invokes the `simplify' tactic
+     * on the goal.
      **/
     public Goal simplify(Params p) throws Z3Exception
     {

src/api/java/IntExpr.java

@@ -23,7 +23,8 @@ package com.microsoft.z3;
 public class IntExpr extends ArithExpr
 {
 	/**
-	 * Constructor for IntExpr </summary>
+	 * Constructor for IntExpr
+	 * @throws Z3Exception on error
 	 **/
 	protected IntExpr(Context ctx) throws Z3Exception
 	{

src/api/java/IntSymbol.java

@@ -25,8 +25,9 @@ import com.microsoft.z3.enumerations.Z3_symbol_kind;
 public class IntSymbol extends Symbol
 {
     /**
-     * The int value of the symbol. <remarks>Throws an exception if the symbol
+     * The int value of the symbol.
-     * is not of int kind. </remarks>
+	 * Remarks: Throws an exception if the symbol
+     * is not of int kind. 
      **/
     public int getInt() throws Z3Exception
     {

src/api/java/InterpolationContext.java

@@ -20,15 +20,13 @@ package com.microsoft.z3;
 import java.util.Map;
 import java.lang.String;
 
-import com.microsoft.z3.Native.IntPtr;
-import com.microsoft.z3.Native.UIntArrayPtr;
 import com.microsoft.z3.enumerations.Z3_lbool;
 
-/** <summary>
+/** 
  *  The InterpolationContext is suitable for generation of interpolants.
- * </summary>
+ *
- * <remarks>For more information on interpolation please refer
+ * Remarks: For more information on interpolation please refer
- * too the C/C++ API, which is well documented.</remarks> 
+ * too the C/C++ API, which is well documented. 
  **/
 public class InterpolationContext extends Context
 {
@@ -44,7 +42,9 @@ public class InterpolationContext extends Context
     /** 
      * Constructor.
      *
-     * <remarks><seealso cref="Context.Context(Dictionary&lt;string, string&gt;)"/></remarks>
+     * 
+	 * Remarks: 
+	 * @see Context#Context
      **/
     public InterpolationContext(Map<String, String> settings) throws Z3Exception
     { 
@@ -58,7 +58,7 @@ public class InterpolationContext extends Context
 
     /** 
       * Create an expression that marks a formula position for interpolation.
-     * @throws Z3Exception 
+      * @throws Z3Exception 
       **/
     public BoolExpr MkInterpolant(BoolExpr a) throws Z3Exception
     {
@@ -68,9 +68,9 @@ public class InterpolationContext extends Context
 
     /**
      * Computes an interpolant.
-     * <remarks>For more information on interpolation please refer
+     * Remarks: For more information on interpolation please refer
      * too the function Z3_get_interpolant in the C/C++ API, which is 
-     * well documented.</remarks>
+     * well documented.
      * @throws Z3Exception 
      **/
     Expr[] GetInterpolant(Expr pf, Expr pat, Params p) throws Z3Exception
@@ -89,9 +89,9 @@ public class InterpolationContext extends Context
 
     /**
      * Computes an interpolant.   
-     * <remarks>For more information on interpolation please refer
+     * Remarks: For more information on interpolation please refer
      * too the function Z3_compute_interpolant in the C/C++ API, which is 
-     * well documented.</remarks>
+     * well documented.
      * @throws Z3Exception 
      **/
     Z3_lbool ComputeInterpolant(Expr pat, Params p, ASTVector interp, Model model) throws Z3Exception
@@ -107,23 +107,23 @@ public class InterpolationContext extends Context
         return Z3_lbool.fromInt(r);
     }
 
-    /// <summary> 
+    ///  
     /// Return a string summarizing cumulative time used for interpolation.
-    /// </summary>    
+    ///    
-    /// <remarks>For more information on interpolation please refer
+    /// Remarks: For more information on interpolation please refer
     /// too the function Z3_interpolation_profile in the C/C++ API, which is 
-    /// well documented.</remarks>
+    /// well documented.
     public String InterpolationProfile() throws Z3Exception
     {
         return Native.interpolationProfile(nCtx());
     }
 
-    /// <summary> 
+    ///  
     /// Checks the correctness of an interpolant.
-    /// </summary>    
+    ///    
-    /// <remarks>For more information on interpolation please refer
+    /// Remarks: For more information on interpolation please refer
     /// too the function Z3_check_interpolant in the C/C++ API, which is 
-    /// well documented.</remarks>
+    /// well documented.
     public int CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory) throws Z3Exception
     {
         Native.StringPtr n_err_str = new Native.StringPtr();
@@ -139,12 +139,12 @@ public class InterpolationContext extends Context
         return r;
     }
 
-    /// <summary> 
+    ///  
     /// Reads an interpolation problem from a file.
-    /// </summary>    
+    ///    
-    /// <remarks>For more information on interpolation please refer
+    /// Remarks: For more information on interpolation please refer
     /// too the function Z3_read_interpolation_problem in the C/C++ API, which is 
-    /// well documented.</remarks>
+    /// well documented.
     public int ReadInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
     {
         Native.IntPtr n_num = new Native.IntPtr();
@@ -170,12 +170,12 @@ public class InterpolationContext extends Context
         return r;
     }
 
-    /// <summary> 
+    ///  
     /// Writes an interpolation problem to a file.
-    /// </summary>    
+    ///    
-    /// <remarks>For more information on interpolation please refer
+    /// Remarks: For more information on interpolation please refer
     /// too the function Z3_write_interpolation_problem in the C/C++ API, which is 
-    /// well documented.</remarks>
+    /// well documented.
     public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) throws Z3Exception
     {
         Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));     

src/api/java/Log.java

@@ -18,17 +18,18 @@ Notes:
 package com.microsoft.z3;
 
 /**
- * Interaction logging for Z3. <remarks> Note that this is a global, static log
+ * Interaction logging for Z3.
+	 * Remarks:  Note that this is a global, static log
  * and if multiple Context objects are created, it logs the interaction with all
- * of them. </remarks>
+ * of them. 
  **/
 public final class Log
 {
     private static boolean m_is_open = false;
 
     /**
-     * Open an interaction log file. <param name="filename">the name of the file
+     * Open an interaction log file. 
-     * to open</param>
+	 * @param filename the name of the file to open
      * 
      * @return True if opening the log file succeeds, false otherwise.
      **/
@@ -48,7 +49,7 @@ public final class Log
     }
 
     /**
-     * Appends the user-provided string <paramref name="s"/> to the interaction
+     * Appends the user-provided string {@code s} to the interaction
      * log.
      * @throws Z3Exception 
      **/

src/api/java/Model.java

@@ -25,8 +25,9 @@ import com.microsoft.z3.enumerations.Z3_sort_kind;
 public class Model extends Z3Object
 {
     /**
-     * Retrieves the interpretation (the assignment) of <paramref name="a"/> in
+     * Retrieves the interpretation (the assignment) of {@code a} in
-     * the model. <param name="a">A Constant</param>
+     * the model. 
+	 * @param a A Constant
      * 
      * @return An expression if the constant has an interpretation in the model,
      *         null otherwise.
@@ -39,8 +40,9 @@ public class Model extends Z3Object
     }
 
     /**
-     * Retrieves the interpretation (the assignment) of <paramref name="f"/> in
+     * Retrieves the interpretation (the assignment) of {@code f} in
-     * the model. <param name="f">A function declaration of zero arity</param>
+     * the model. 
+	 * @param f A function declaration of zero arity
      * 
      * @return An expression if the function has an interpretation in the model,
      *         null otherwise.
@@ -65,9 +67,8 @@ public class Model extends Z3Object
     }
 
     /**
-     * Retrieves the interpretation (the assignment) of a non-constant <paramref
+     * Retrieves the interpretation (the assignment) of a non-constant {@code f} in the model. 
-     * name="f"/> in the model. <param name="f">A function declaration of
+	 * @param f A function declaration of non-zero arity
-     * non-zero arity</param>
      * 
      * @return A FunctionInterpretation if the function has an interpretation in
      *         the model, null otherwise.
@@ -196,16 +197,15 @@ public class Model extends Z3Object
     }
 
     /**
-     * Evaluates the expression <paramref name="t"/> in the current model.
+     * Evaluates the expression {@code t} in the current model.
-     * <remarks> This function may fail if <paramref name="t"/> contains
+     * Remarks:  This function may fail if {@code t} contains
-     * quantifiers, is partial (MODEL_PARTIAL enabled), or if <paramref
+     * quantifiers, is partial (MODEL_PARTIAL enabled), or if {@code t} is not well-sorted. In this case a
-     * name="t"/> is not well-sorted. In this case a
+     * {@code ModelEvaluationFailedException} is thrown.  
-     * <code>ModelEvaluationFailedException</code> is thrown. </remarks> <param
+	 * @param t An expression {@code completion} When this flag
-     * name="t">An expression</param> <param name="completion"> When this flag
      * is enabled, a model value will be assigned to any constant or function
-     * that does not have an interpretation in the model. </param>
+     * that does not have an interpretation in the model.
      * 
-     * @return The evaluation of <paramref name="t"/> in the model.
+     * @return The evaluation of {@code t} in the model.
      * @throws Z3Exception
      **/
     public Expr eval(Expr t, boolean completion) throws Z3Exception
@@ -219,7 +219,7 @@ public class Model extends Z3Object
     }
 
     /**
-     * Alias for <code>Eval</code>.
+     * Alias for {@code Eval}.
      * 
      * @throws Z3Exception
      **/
@@ -239,10 +239,12 @@ public class Model extends Z3Object
 
     /**
      * The uninterpreted sorts that the model has an interpretation for.
-     * <remarks> Z3 also provides an intepretation for uninterpreted sorts used
+     * Remarks:  Z3 also provides an intepretation for uninterpreted sorts used
      * in a formula. The interpretation for a sort is a finite set of distinct
-     * values. We say this finite set is the "universe" of the sort. </remarks>
+     * values. We say this finite set is the "universe" of the sort. 
-     * <seealso cref="NumSorts"/> <seealso cref="SortUniverse"/>
+     * 
+	 * @see getNumSorts
+	 * @see getSortUniverse
      * 
      * @throws Z3Exception
      **/
@@ -259,11 +261,11 @@ public class Model extends Z3Object
 
     /**
      * The finite set of distinct values that represent the interpretation for
-     * sort <paramref name="s"/>. <seealso cref="Sorts"/> <param name="s">An
+     * sort {@code s}. 
-     * uninterpreted sort</param>
+	 * @param s An uninterpreted sort
      * 
      * @return An array of expressions, where each is an element of the universe
-     *         of <paramref name="s"/>
+     *         of {@code s}
      * @throws Z3Exception
      **/
     public Expr[] getSortUniverse(Sort s) throws Z3Exception

src/api/java/Probe.java

@@ -21,8 +21,8 @@ package com.microsoft.z3;
  * Probes are used to inspect a goal (aka problem) and collect information that
  * may be used to decide which solver and/or preprocessing step will be used.
  * The complete list of probes may be obtained using the procedures
- * <code>Context.NumProbes</code> and <code>Context.ProbeNames</code>. It may
+ * {@code Context.NumProbes} and {@code Context.ProbeNames}. It may
- * also be obtained using the command <code>(help-tactics)</code> in the SMT 2.0
+ * also be obtained using the command {@code (help-tactics)} in the SMT 2.0
  * front-end.
  **/
 public class Probe extends Z3Object

src/api/java/RatNum.java

@@ -61,8 +61,9 @@ public class RatNum extends RealExpr
     }
 
     /**
-     * Returns a string representation in decimal notation. <remarks>The result
+     * Returns a string representation in decimal notation.
-     * has at most <paramref name="precision"/> decimal places.</remarks>
+	 * Remarks: The result
+     * has at most {@code precision} decimal places.
      **/
     public String toDecimalString(int precision) throws Z3Exception
     {

src/api/java/RealExpr.java

@@ -23,7 +23,7 @@ package com.microsoft.z3;
 public class RealExpr extends ArithExpr
 {
     /**
-     * Constructor for RealExpr </summary>
+     * Constructor for RealExpr
      **/
     protected RealExpr(Context ctx)
     {

src/api/java/Solver.java

@@ -56,8 +56,9 @@ public class Solver extends Z3Object
     }
 
     /**
-     * The current number of backtracking points (scopes). <seealso cref="Pop"/>
+     * The current number of backtracking points (scopes). 
-     * <seealso cref="Push"/>
+	 * @see pop 
+	 * @see push
      **/
     public int getNumScopes() throws Z3Exception
     {
@@ -66,7 +67,8 @@ public class Solver extends Z3Object
     }
 
     /**
-     * Creates a backtracking point. <seealso cref="Pop"/>
+     * Creates a backtracking point. 
+	 * @see pop
      **/
     public void push() throws Z3Exception
     {
@@ -74,7 +76,8 @@ public class Solver extends Z3Object
     }
 
     /**
-     * Backtracks one backtracking point. <remarks>.
+     * Backtracks one backtracking point.
+	 * Remarks: .
      **/
     public void pop() throws Z3Exception
     {
@@ -82,9 +85,11 @@ public class Solver extends Z3Object
     }
 
     /**
-     * Backtracks <paramref name="n"/> backtracking points. <remarks>Note that
+     * Backtracks {@code n} backtracking points.
-     * an exception is thrown if <paramref name="n"/> is not smaller than
+	 * Remarks: Note that
-     * <code>NumScopes</code></remarks> <seealso cref="Push"/>
+     * an exception is thrown if {@code n} is not smaller than
+     * {@code NumScopes} 
+	 * @see push
      **/
     public void pop(int n) throws Z3Exception
     {
@@ -92,8 +97,9 @@ public class Solver extends Z3Object
     }
 
     /**
-     * Resets the Solver. <remarks>This removes all assertions from the
+     * Resets the Solver.
-     * solver.</remarks>
+	 * Remarks: This removes all assertions from the
+     * solver.
      **/
     public void reset() throws Z3Exception
     {
@@ -115,12 +121,12 @@ public class Solver extends Z3Object
         }
     }
 
-    // / <summary>
+    // / 
     // / Assert multiple constraints into the solver, and track them (in the
     // unsat) core
     // / using the Boolean constants in ps.
-    // / </summary>
+    // /
-    // / <remarks>
+    // / Remarks: 
     // / This API is an alternative to <see cref="Check"/> with assumptions for
     // extracting unsat cores.
     // / Both APIs can be used in the same solver. The unsat core will contain a
@@ -128,7 +134,7 @@ public class Solver extends Z3Object
     // / of the Boolean variables provided using <see cref="AssertAndTrack"/>
     // and the Boolean literals
     // / provided using <see cref="Check"/> with assumptions.
-    // / </remarks>
+    // / 
     public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) throws Z3Exception
     {
         getContext().checkContextMatch(constraints);
@@ -141,11 +147,11 @@ public class Solver extends Z3Object
                     constraints[i].getNativeObject(), ps[i].getNativeObject());
     }
 
-    // / <summary>
+    // / 
     // / Assert a constraint into the solver, and track it (in the unsat) core
     // / using the Boolean constant p.
-    // / </summary>
+    // /
-    // / <remarks>
+    // / Remarks: 
     // / This API is an alternative to <see cref="Check"/> with assumptions for
     // extracting unsat cores.
     // / Both APIs can be used in the same solver. The unsat core will contain a
@@ -153,7 +159,7 @@ public class Solver extends Z3Object
     // / of the Boolean variables provided using <see cref="AssertAndTrack"/>
     // and the Boolean literals
     // / provided using <see cref="Check"/> with assumptions.
-    // / </remarks>
+    // / 
     public void assertAndTrack(BoolExpr constraint, BoolExpr p) throws Z3Exception
     {
         getContext().checkContextMatch(constraint);
@@ -193,8 +199,10 @@ public class Solver extends Z3Object
 
     /**
      * Checks whether the assertions in the solver are consistent or not.
-     * <remarks> <seealso cref="Model"/> <seealso cref="UnsatCore"/> <seealso
+     * Remarks:  
-     * cref="Proof"/> </remarks>
+	 * @see getModel
+	 * @see getUnsatCore
+	 * @see getProof 
      **/
     public Status check(Expr... assumptions) throws Z3Exception
     {
@@ -219,8 +227,10 @@ public class Solver extends Z3Object
 
     /**
      * Checks whether the assertions in the solver are consistent or not.
-     * <remarks> <seealso cref="Model"/> <seealso cref="UnsatCore"/> <seealso
+     * Remarks:  
-     * cref="Proof"/> </remarks>
+	 * @see getModel
+	 * @see getUnsatCore
+	 * @see getProof 
      **/
     public Status check() throws Z3Exception
     {
@@ -228,10 +238,11 @@ public class Solver extends Z3Object
     }
 
     /**
-     * The model of the last <code>Check</code>. <remarks> The result is
+     * The model of the last {@code Check}.
-     * <code>null</code> if <code>Check</code> was not invoked before, if its
+	 * Remarks:  The result is
-     * results was not <code>SATISFIABLE</code>, or if model production is not
+     * {@code null} if {@code Check} was not invoked before, if its
-     * enabled. </remarks>
+     * results was not {@code SATISFIABLE}, or if model production is not
+     * enabled. 
      * 
      * @throws Z3Exception
      **/
@@ -245,10 +256,11 @@ public class Solver extends Z3Object
     }
 
     /**
-     * The proof of the last <code>Check</code>. <remarks> The result is
+     * The proof of the last {@code Check}.
-     * <code>null</code> if <code>Check</code> was not invoked before, if its
+	 * Remarks:  The result is
-     * results was not <code>UNSATISFIABLE</code>, or if proof production is
+     * {@code null} if {@code Check} was not invoked before, if its
-     * disabled. </remarks>
+     * results was not {@code UNSATISFIABLE}, or if proof production is
+     * disabled. 
      * 
      * @throws Z3Exception
      **/
@@ -262,10 +274,11 @@ public class Solver extends Z3Object
     }
 
     /**
-     * The unsat core of the last <code>Check</code>. <remarks> The unsat core
+     * The unsat core of the last {@code Check}.
-     * is a subset of <code>Assertions</code> The result is empty if
+	 * Remarks:  The unsat core
-     * <code>Check</code> was not invoked before, if its results was not
+     * is a subset of {@code Assertions} The result is empty if
-     * <code>UNSATISFIABLE</code>, or if core production is disabled. </remarks>
+     * {@code Check} was not invoked before, if its results was not
+     * {@code UNSATISFIABLE}, or if core production is disabled. 
      * 
      * @throws Z3Exception
      **/
@@ -282,8 +295,8 @@ public class Solver extends Z3Object
     }
 
     /**
-     * A brief justification of why the last call to <code>Check</code> returned
+     * A brief justification of why the last call to {@code Check} returned
-     * <code>UNKNOWN</code>.
+     * {@code UNKNOWN}.
      **/
     public String getReasonUnknown() throws Z3Exception
     {

src/api/java/Sort.java

@@ -28,8 +28,8 @@ public class Sort extends AST
     /* Overloaded operators are not translated. */
 
     /**
-     * Equality operator for objects of type Sort. <param name="o"/>
+     * Equality operator for objects of type Sort. 
-     * 
+	 * @param o
      * @return
      **/
     public boolean equals(Object o)

src/api/java/Statistics.java

@@ -24,7 +24,7 @@ public class Statistics extends Z3Object
 {
     /**
      * Statistical data is organized into pairs of [Key, Entry], where every
-     * Entry is either a <code>DoubleEntry</code> or a <code>UIntEntry</code>
+     * Entry is either a {@code DoubleEntry} or a {@code UIntEntry}
      **/
     public class Entry
     {
@@ -176,8 +176,9 @@ public class Statistics extends Z3Object
     }
 
     /**
-     * The value of a particular statistical counter. <remarks>Returns null if
+     * The value of a particular statistical counter.
-     * the key is unknown.</remarks>
+	 * Remarks: Returns null if
+     * the key is unknown.
      * 
      * @throws Z3Exception
      **/

src/api/java/StringSymbol.java

@@ -25,8 +25,9 @@ import com.microsoft.z3.enumerations.Z3_symbol_kind;
 public class StringSymbol extends Symbol
 {
     /**
-     * The string value of the symbol. <remarks>Throws an exception if the
+     * The string value of the symbol.
-     * symbol is not of string kind.</remarks>
+	 * Remarks: Throws an exception if the
+     * symbol is not of string kind.
      **/
     public String getString() throws Z3Exception
     {

src/api/java/Tactic.java

@@ -20,8 +20,8 @@ package com.microsoft.z3;
 /**
  * Tactics are the basic building block for creating custom solvers for specific
  * problem domains. The complete list of tactics may be obtained using
- * <code>Context.NumTactics</code> and <code>Context.TacticNames</code>. It may
+ * {@code Context.NumTactics} and {@code Context.TacticNames}. It may
- * also be obtained using the command <code>(help-tactics)</code> in the SMT 2.0
+ * also be obtained using the command {@code (help-tactics)} in the SMT 2.0
  * front-end.
  **/
 public class Tactic extends Z3Object
@@ -73,8 +73,8 @@ public class Tactic extends Z3Object
     }
 
     /**
-     * Creates a solver that is implemented using the given tactic. <seealso
+     * Creates a solver that is implemented using the given tactic. 
-     * cref="Context.MkSolver(Tactic)"/>
+	 * @see Context#mkSolver(Tactic)
      * @throws Z3Exception 
      **/
     public Solver getSolver() throws Z3Exception

src/api/java/Version.java

@@ -18,7 +18,8 @@ Notes:
 package com.microsoft.z3;
 
 /**
- * Version information. <remarks>Note that this class is static.</remarks>
+ * Version information. 
+	 * Remarks: Note that this class is static.
  **/
 public class Version
 {

src/api/python/z3.py

@@ -3813,6 +3813,18 @@ def RepeatBitVec(n, a):
         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
     return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
 
+def BVRedAnd(a):
+    """Return the reduction-and expression of `a`."""
+    if __debug__:
+        _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
+    return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
+
+def BVRedOr(a):
+    """Return the reduction-or expression of `a`."""
+    if __debug__:
+        _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression")
+    return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
+
 #########################################
 #
 # Arrays
@@ -6046,7 +6058,7 @@ class Solver(Z3PPObject):
             e = es[sz1].as_ast()
         else:
             e = BoolVal(True, self.ctx).as_ast()
-            return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
+        return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
 
 
 

src/duality/duality.h

@@ -778,6 +778,10 @@ protected:
       struct Bad {
       };
       
+      // thrown on more serious internal error
+      struct ReallyBad {
+      };
+
       /** Pop a scope (see Push). Note, you cannot pop axioms. */
       
       void Pop(int num_scopes);

src/duality/duality_rpfp.cpp

@@ -2643,6 +2643,10 @@ namespace Duality {
 	GetGroundLitsUnderQuants(memo,f.body(),res,1);
       return;
     }
+    if(f.is_var()){
+      //      std::cout << "foo!\n";
+      return;
+    }
     if(under && f.is_ground())
       res.push_back(f);
   }
@@ -3065,10 +3069,14 @@ namespace Duality {
     node->Annotation.SetEmpty();
     hash_set<ast> *core = new hash_set<ast>;
     core->insert(node->Outgoing->dual);
+    expr prev_annot = ctx.bool_val(false);
+    expr prev_impl = ctx.bool_val(false);
+    int repeated_case_count = 0;
     while(1){
       by_case_counter++;
       is.push();
       expr annot = !GetAnnotation(node);
+      Transformer old_annot = node->Annotation;
       is.add(annot);
       if(is.check() == unsat){
 	is.pop(1);
@@ -3076,56 +3084,70 @@ namespace Duality {
       }
       is.pop(1);
       Push();
-      ConstrainEdgeLocalized(node->Outgoing,is.get_implicant());
+      expr the_impl = is.get_implicant();
+      if(eq(the_impl,prev_impl)){
+	//	std::cout << "got old implicant\n";
+	repeated_case_count++;
+      }
+      prev_impl = the_impl;
+      ConstrainEdgeLocalized(node->Outgoing,the_impl);
       ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this?
-      check_result foo = Check(root);
-      if(foo != unsat){
-	slvr().print("should_be_unsat.smt2");
-	throw "should be unsat";
-      }
-      std::vector<expr> assumps, axioms_to_add;
-      slvr().get_proof().get_assumptions(assumps);
-      for(unsigned i = 0; i < assumps.size(); i++){
-	(*core).insert(assumps[i]);
-	if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
-	  axioms_to_add.push_back(assumps[i]);
-	  axioms_needed.erase(assumps[i]);
-	}
-      }
-      // AddToProofCore(*core);
-      Transformer old_annot = node->Annotation;
-      SolveSingleNode(root,node);
-
-      {
-	expr itp = GetAnnotation(node);
-	dualModel = is.get_model(); // TODO: what does this mean?
-	std::vector<expr> case_lits;
-	itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
-	SetAnnotation(node,itp);
-	node->Annotation.Formula = node->Annotation.Formula.simplify();
-      }
-
-      for(unsigned i = 0; i < axioms_to_add.size(); i++)
-	is.add(axioms_to_add[i]);
       
-#define TEST_BAD
-#ifdef TEST_BAD
       {
-	static int bad_count = 0, num_bads = 1;
+	check_result foo = Check(root);
-	if(bad_count >= num_bads){
+	if(foo != unsat){
-	  bad_count = 0;
-	  num_bads = num_bads * 2;
 	  Pop(1);
 	  is.pop(1);
 	  delete core;
 	  timer_stop("InterpolateByCases");
-	  throw Bad();
+	  throw ReallyBad();
+	  // slvr().print("should_be_unsat.smt2");
+	  // throw "should be unsat";
 	}
-	bad_count++;
+	std::vector<expr> assumps, axioms_to_add;
-      }
+	slvr().get_proof().get_assumptions(assumps);
-#endif
+	for(unsigned i = 0; i < assumps.size(); i++){
+	  (*core).insert(assumps[i]);
+	  if(axioms_needed.find(assumps[i]) != axioms_needed.end()){
+	    axioms_to_add.push_back(assumps[i]);
+	    axioms_needed.erase(assumps[i]);
+	  }
+	}
+	// AddToProofCore(*core);
+	SolveSingleNode(root,node);
 
-      if(node->Annotation.IsEmpty()){
+	{
+	  expr itp = GetAnnotation(node);
+	  dualModel = is.get_model(); // TODO: what does this mean?
+	  std::vector<expr> case_lits;
+	  itp = StrengthenFormulaByCaseSplitting(itp, case_lits);
+	  SetAnnotation(node,itp);
+	  node->Annotation.Formula = node->Annotation.Formula.simplify();
+	}
+
+	for(unsigned i = 0; i < axioms_to_add.size(); i++)
+	  is.add(axioms_to_add[i]);
+      
+#define TEST_BAD
+#ifdef TEST_BAD
+	{
+	  static int bad_count = 0, num_bads = 1;
+	  if(bad_count >= num_bads){
+	    bad_count = 0;
+	    num_bads = num_bads * 2;
+	    Pop(1);
+	    is.pop(1);
+	    delete core;
+	    timer_stop("InterpolateByCases");
+	    throw Bad();
+	  }
+	  bad_count++;
+	}
+#endif
+      }
+
+      if(node->Annotation.IsEmpty() || eq(node->Annotation.Formula,prev_annot) || (repeated_case_count > 0 && !axioms_added) || (repeated_case_count >= 10)){
+      looks_bad:
 	if(!axioms_added){
 	  // add the axioms in the off chance they are useful
 	  const std::vector<expr> &theory = ls->get_axioms();
@@ -3134,6 +3156,7 @@ namespace Duality {
 	  axioms_added = true;
 	}
 	else {
+	  //#define KILL_ON_BAD_INTERPOLANT	  
 #ifdef KILL_ON_BAD_INTERPOLANT	  
 	  std::cout << "bad in InterpolateByCase -- core:\n";
 #if 0
@@ -3175,10 +3198,11 @@ namespace Duality {
 	  is.pop(1);
 	  delete core;
 	  timer_stop("InterpolateByCases");
-	  throw Bad();
+	  throw ReallyBad();
 	}
       }
       Pop(1);
+      prev_annot = node->Annotation.Formula;
       node->Annotation.UnionWith(old_annot);
     }
     if(proof_core)

src/duality/duality_solver.cpp

@@ -2279,6 +2279,18 @@ namespace Duality {
 		  // bad interpolants can get us here
 		  throw DoRestart();
 		}
+		catch(const RPFP::ReallyBad &){
+		  // this could be caused by incompleteness
+		  for(unsigned i = 0; i < expansions.size(); i++){
+		    Node *node = expansions[i];
+		    node->map->Annotation.SetFull();
+		    std::vector<Node *> &chs = node->map->Outgoing->Children;
+		    for(unsigned j = 0; j < chs.size(); j++)
+		      chs[j]->Annotation.SetFull();
+		    reporter->Message("incompleteness: cleared annotation and child annotations");
+		  }
+		  throw DoRestart();
+		}
 		catch(char const *msg){
 		  // bad interpolants can get us here
 		  reporter->Message(std::string("interpolation failure:") + msg);

src/interp/iz3mgr.cpp

@@ -778,6 +778,8 @@ int iz3mgr::occurs_in(ast var, ast e){
 
 
 bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){
+  if(occurs_in(v,y))
+    return false;
   if(op(x) == Plus){
     int n = num_args(x);
     for(int i = 0; i < n; i++){
@@ -801,8 +803,8 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set<ast> &cont_eq_memo, bool truth, as
     return ast();
   cont_eq_memo.insert(e);
   if(!truth && op(e) == Equal){
-    if(arg(e,0) == v) return(arg(e,1));
+    if(arg(e,0) == v && !occurs_in(v,arg(e,1))) return(arg(e,1));
-    if(arg(e,1) == v) return(arg(e,0));
+    if(arg(e,1) == v && !occurs_in(v,arg(e,0))) return(arg(e,0));
     ast res;
     if(solve_arith(v,arg(e,0),arg(e,1),res)) return res;
     if(solve_arith(v,arg(e,1),arg(e,0),res)) return res;

src/interp/iz3mgr.h

@@ -278,7 +278,8 @@ class iz3mgr  {
   }
 
   symb sym(ast t){
-    return to_app(t.raw())->get_decl();
+    raw_ast *_ast = t.raw();
+    return is_app(_ast) ? to_app(_ast)->get_decl() : 0;
   }
 
   std::string string_of_symbol(symb s){

src/interp/iz3proof_itp.cpp

@@ -1027,7 +1027,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	linear_comb(Aineqs,coeff,make(Leq,make_int(rational(0)),make(Sub,term2,term1)));
     }
     else {
-      ast pf = extract_rewrites(make(concat,mk_true(),rest),p1);
+      ast pf = extract_rewrites(make(concat,mk_true(),last),p1);
       ast new_normal = fix_normal(term1,term2,pf);
       normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
     }

src/interp/iz3translate.cpp

@@ -1712,11 +1712,17 @@ public:
 	std::cout << "foo!\n";
 
       // no idea why this shows up
-      if(dk == PR_MODUS_PONENS_OEQ)
+      if(dk == PR_MODUS_PONENS_OEQ){
 	if(conc(prem(proof,0)) == con){
 	  res = translate_main(prem(proof,0),expect_clause);
 	  return res;
 	}
+	if(expect_clause && op(con) == Or){ // skolemization does this
+	  Iproof::node clause = translate_main(prem(proof,0),true);
+	  res = RewriteClause(clause,prem(proof,1));
+	  return res;
+	}
+      }
       
 #if 0
       if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
@@ -1800,7 +1806,9 @@ public:
 	}
 	break;
       }
-      case PR_MONOTONICITY: {
+      case PR_QUANT_INTRO:
+      case PR_MONOTONICITY:
+	{
 	std::vector<ast> eqs; eqs.resize(args.size());
 	for(unsigned i = 0; i < args.size(); i++)
 	  eqs[i] = conc(prem(proof,i));

src/smt/smt_context.cpp

@@ -3321,13 +3321,13 @@ namespace smt {
                 CASSERT("dyn_ack", check_clauses(m_lemmas) && check_clauses(m_aux_clauses));
             }
             
-            if (resource_limits_exceeded()) {
+            if (resource_limits_exceeded() && !inconsistent()) {
-                SASSERT(!inconsistent());
                 return l_undef;
             }
 
             if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses)
                 simplify_clauses();
+
             
             if (!decide()) {
                 final_check_status fcs = final_check();
@@ -3342,8 +3342,7 @@ namespace smt {
                 }
             }
 
-            if (resource_limits_exceeded()) {
+            if (resource_limits_exceeded() && !inconsistent()) {
-                SASSERT(!inconsistent());
                 return l_undef;
             }
         }

src/smt/theory_arith_core.h

@@ -336,8 +336,9 @@ namespace smt {
     theory_var theory_arith<Ext>::internalize_rem(app * n) {
         theory_var s  = mk_binary_op(n);
         context & ctx = get_context();
-        if (!ctx.relevancy())
+        if (!ctx.relevancy()) {
             mk_rem_axiom(n->get_arg(0), n->get_arg(1));
+        }
         return s;
     }
 
@@ -456,22 +457,20 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::mk_rem_axiom(expr * dividend, expr * divisor) {
-        if (!m_util.is_zero(divisor)) {
+        // if divisor is zero, then rem is an uninterpreted function.
-            // if divisor is zero, then rem is an uninterpreted function.
+        ast_manager & m    = get_manager();
-            ast_manager & m    = get_manager();
+        expr * zero        = m_util.mk_numeral(rational(0), true);
-            expr * zero        = m_util.mk_numeral(rational(0), true);
+        expr * rem         = m_util.mk_rem(dividend, divisor);
-            expr * rem         = m_util.mk_rem(dividend, divisor);
+        expr * mod         = m_util.mk_mod(dividend, divisor);
-            expr * mod         = m_util.mk_mod(dividend, divisor);
+        expr_ref dltz(m), eq1(m), eq2(m);
-            expr_ref dltz(m), eq1(m), eq2(m);
+        dltz               = m_util.mk_lt(divisor, zero);
-            dltz               = m_util.mk_lt(divisor, zero);
+        eq1                = m.mk_eq(rem, mod);
-            eq1                = m.mk_eq(rem, mod);
+        eq2                = m.mk_eq(rem, m_util.mk_sub(zero, mod));
-            eq2                = m.mk_eq(rem, m_util.mk_sub(zero, mod));
+        // n < 0 || rem(a,n) = mod(a, n)
-            // n < 0 || rem(a,n) = mod(a, n)
+        mk_axiom(dltz, eq1);
-            mk_axiom(dltz, eq1);
+        dltz               = m.mk_not(dltz);
-            dltz               = m.mk_not(dltz);
+        // !n < 0 || rem(a,n) = -mod(a, n)
-            // !n < 0 || rem(a,n) = -mod(a, n)
+        mk_axiom(dltz, eq2);        
-            mk_axiom(dltz, eq2);
-        }
     }
 
     //