title: Giving a Z3 solver a complete model to analyze (Using the .Net Api)
body: <p>I am building a model for the Z3 analyzer. As this model has huge number of constraints and all these constraints are build one by one, all this process is using different Z3 Apis. As a result when I look at the over all time that the process of building the model takes it is an extremely long time. Some times even my laptop is short on memory and can't complete the model creation process. To solve this problem I was looking for building the required model as a text file and feeding the completed model to the Z3 solver. Theoretically this should improve the timing issue as I will be calling the Z3 Api only once. As I looked around the only thing I could find was to use a function named 'Z3_benchmark_to_smtlib_string' which is available in the python Api of Z3. I was wondering if this function, or a simillar function, is also available in the .Net Api of the Z3?
  I will try to explain this with a small example:
  I am initially using Z3 Solver like this:</p>
  <pre><code>    public void Solver_Test()
      {
          BoolExpr lA = cICtx.MkBoolConst(&quot;A&quot;);
          cISolver.Assert(lA);
  
          cISolver.Check();
  
          Model lResultModel = cISolver.Model;
  
          foreach (FuncDecl lFunctionDecleration in lResultModel.ConstDecls)
          {
              
          }
  
      }
  </code></pre>
  <p>But I want to be able to use it like this:</p>
  <pre><code>    public void Solver_Test()
      {
          string lSolverConstraintStr = &quot;&quot;;
  
          lSolverConstraintStr += &quot;(declare-const A Bool)&quot;;
          lSolverConstraintStr += &quot;(assert A)&quot;;
  
          //Somehow add the &quot;lSolverConstraintStr&quot; to my &quot;cISolver&quot;
  
          cISolver.Check();
  
          Model lResultModel = cISolver.Model;
  
          foreach (FuncDecl lFunctionDecleration in lResultModel.ConstDecls)
          {
              
          }
  
      }
  </code></pre>
  <p>Is there a way of doing this?</p>